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

Theorem intnand 917
 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 109 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 618 1 (𝜑 → ¬ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-in1 604  ax-in2 605 This theorem is referenced by:  dcan  919  poxp  6176  cauappcvgprlemladdrl  7571  caucvgprlemladdrl  7592  xrrebnd  9716  fzpreddisj  9966  fzp1nel  9999  fprodntrivap  11474  gcdsupex  11832  gcdsupcl  11833  gcdnncl  11842  gcd2n0cl  11844  qredeu  11965  cncongr2  11972  divnumden  12061  divdenle  12062  phisum  12103  ivthinclemdisj  12989
 Copyright terms: Public domain W3C validator