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

Theorem intnand 874
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
Hypothesis
Ref Expression
intnand.1  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
intnand  |-  ( ph  ->  -.  ( ch  /\  ps ) )

Proof of Theorem intnand
StepHypRef Expression
1 intnand.1 . 2  |-  ( ph  ->  -.  ps )
2 simpr 108 . 2  |-  ( ( ch  /\  ps )  ->  ps )
31, 2nsyl 591 1  |-  ( ph  ->  -.  ( ch  /\  ps ) )
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 577  ax-in2 578
This theorem is referenced by:  dcan  876  poxp  5932  cauappcvgprlemladdrl  7119  caucvgprlemladdrl  7140  xrrebnd  9176  fzpreddisj  9378  fzp1nel  9411  gcdsupex  10729  gcdsupcl  10730  gcdnncl  10739  gcd2n0cl  10741  qredeu  10859  cncongr2  10866  divnumden  10954  divdenle  10955
  Copyright terms: Public domain W3C validator