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

Theorem intnand 899
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 600 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 586  ax-in2 587
This theorem is referenced by:  dcan  901  poxp  6095  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  xrrebnd  9553  fzpreddisj  9802  fzp1nel  9835  gcdsupex  11553  gcdsupcl  11554  gcdnncl  11563  gcd2n0cl  11565  qredeu  11685  cncongr2  11692  divnumden  11780  divdenle  11781  ivthinclemdisj  12693
  Copyright terms: Public domain W3C validator