Theorem intnanrd 494

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 487	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 141	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

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

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 210  df-an 401

This theorem is referenced by:  bianfd  543  3bior1fand  1504  pr1eqbg  4823  iresn0n0  6054  frxp2  8136  frxp3  8143  wemappo  9507  axrepnd  10575  axunnd  10577  fzpreddisj  13597  sadadd2lem2  16504  smumullem  16546  nndvdslegcd  16559  divgcdnn  16569  sqgcd  16616  coprm  16766  isnmnd  18792  nfimdetndef  22711  mdetfval1  22712  ibladdlem  25944  lgsval2lem  27433  lgsval4a  27445  lgsdilem  27450  2sqcoprm  27561  addsqn2reurex2  27571  nosepdmlem  27809  nodenselem8  27817  nosupbnd2lem1  27841  pw2cut2  28617  nbgrnself  29646  wwlks  30121  iswspthsnon  30142  clwwlknon1nloop  30387  clwwlknon1le1  30389  nfrgr2v  30560  tpssad  32822  hashxpe  33089  esplyind  33906  acycgr0v  35535  prclisacycgr  35538  fmlasucdisj  35786  dfrdg4  36338  nmulprop  36577  finxpreclem3  37922  finxpreclem5  37924  ibladdnclem  38210  dihatlat  41993  xppss12  42883  jm2.23  43608  rexanuz2nf  46091  ltnelicc  46098  limciccioolb  46222  dvmptfprodlem  46543  stoweidlem26  46625  fourierdlem12  46718  fourierdlem42  46748  divgcdoddALTV  48329