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

Theorem intnand 901
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 109 . 2  |-  ( ( ch  /\  ps )  ->  ps )
31, 2nsyl 602 1  |-  ( ph  ->  -.  ( ch  /\  ps ) )
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 588  ax-in2 589
This theorem is referenced by:  dcan  903  poxp  6097  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  xrrebnd  9570  fzpreddisj  9819  fzp1nel  9852  gcdsupex  11573  gcdsupcl  11574  gcdnncl  11583  gcd2n0cl  11585  qredeu  11705  cncongr2  11712  divnumden  11801  divdenle  11802  ivthinclemdisj  12714
  Copyright terms: Public domain W3C validator