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  1474  pr1eqbg  4856  iresn0n0  6052  fvmptopabOLD  7466  frxp2  8132  frxp3  8139  wemappo  9546  axrepnd  10591  axunnd  10593  fzpreddisj  13554  sadadd2lem2  16395  smumullem  16437  nndvdslegcd  16450  divgcdnn  16460  sqgcd  16506  coprm  16652  isnmnd  18663  nfimdetndef  22311  mdetfval1  22312  ibladdlem  25569  lgsval2lem  27046  lgsval4a  27058  lgsdilem  27063  2sqcoprm  27174  addsqn2reurex2  27184  nosepdmlem  27422  nodenselem8  27430  nosupbnd2lem1  27454  nbgrnself  28883  wwlks  29356  iswspthsnon  29377  clwwlknon1nloop  29619  clwwlknon1le1  29621  nfrgr2v  29792  hashxpe  32286  acycgr0v  34437  prclisacycgr  34440  fmlasucdisj  34688  dfrdg4  35227  finxpreclem3  36577  finxpreclem5  36579  ibladdnclem  36847  dihatlat  40508  xppss12  41353  jm2.23  42037  rexanuz2nf  44501  ltnelicc  44508  limciccioolb  44635  dvmptfprodlem  44958  stoweidlem26  45040  fourierdlem12  45133  fourierdlem42  45163  divgcdoddALTV  46648