Theorem intnanrd 488

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnanrd	⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpl 481	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  bianfd  533  3bior1fand  1472  pr1eqbg  4862  iresn0n0  6062  fvmptopabOLD  7481  frxp2  8155  frxp3  8162  wemappo  9580  axrepnd  10625  axunnd  10627  fzpreddisj  13590  sadadd2lem2  16432  smumullem  16474  nndvdslegcd  16487  divgcdnn  16497  sqgcd  16543  coprm  16689  isnmnd  18705  nfimdetndef  22511  mdetfval1  22512  ibladdlem  25769  lgsval2lem  27260  lgsval4a  27272  lgsdilem  27277  2sqcoprm  27388  addsqn2reurex2  27398  nosepdmlem  27636  nodenselem8  27644  nosupbnd2lem1  27668  nbgrnself  29192  wwlks  29666  iswspthsnon  29687  clwwlknon1nloop  29929  clwwlknon1le1  29931  nfrgr2v  30102  hashxpe  32597  acycgr0v  34791  prclisacycgr  34794  fmlasucdisj  35042  dfrdg4  35580  finxpreclem3  36905  finxpreclem5  36907  ibladdnclem  37182  dihatlat  40839  xppss12  41748  jm2.23  42448  rexanuz2nf  44904  ltnelicc  44911  limciccioolb  45038  dvmptfprodlem  45361  stoweidlem26  45443  fourierdlem12  45536  fourierdlem42  45566  divgcdoddALTV  47051

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »