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

Theorem intnand 932
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 110 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 629 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 615  ax-in2 616
This theorem is referenced by:  dcan  934  poxp  6250  cauappcvgprlemladdrl  7673  caucvgprlemladdrl  7694  xrrebnd  9836  fzpreddisj  10088  fzp1nel  10121  fprodntrivap  11609  gcdsupex  11975  gcdsupcl  11976  gcdnncl  11985  gcd2n0cl  11987  qredeu  12114  cncongr2  12121  divnumden  12213  divdenle  12214  phisum  12257  pythagtriplem4  12285  pythagtriplem8  12289  pythagtriplem9  12290  isnsgrp  12834  ivthinclemdisj  14501  lgsneg  14808
  Copyright terms: Public domain W3C validator