ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  intnand GIF version

Theorem intnand 878
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
StepHypRef Expression
1 intnand.1 . 2 (𝜑 → ¬ 𝜓)
2 simpr 108 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 593 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-in1 579  ax-in2 580
This theorem is referenced by:  dcan  880  poxp  5979  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  xrrebnd  9250  fzpreddisj  9452  fzp1nel  9485  gcdsupex  11031  gcdsupcl  11032  gcdnncl  11041  gcd2n0cl  11043  qredeu  11161  cncongr2  11168  divnumden  11256  divdenle  11257
  Copyright terms: Public domain W3C validator