Theorem intnand 943

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

Hypothesis

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

Assertion

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

Proof of Theorem intnand

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpr 110	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 637	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  poxp  6468  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  xrrebnd  10221  fzpreddisj  10478  fzp1nel  10511  fprodntrivap  12351  bitsfzo  12722  bitsmod  12723  gcdsupex  12734  gcdsupcl  12735  gcdnncl  12744  gcd2n0cl  12746  qredeu  12875  cncongr2  12882  divnumden  12974  divdenle  12975  phisum  13019  pythagtriplem4  13047  pythagtriplem8  13051  pythagtriplem9  13052  isnsgrp  13721  ivthinclemdisj  15741  lgsneg  16143  umgredgnlp  16393  umgr2edg1  16450  umgr2edgneu  16453