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

Theorem intnand 917
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 618 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 604  ax-in2 605
This theorem is referenced by:  dcan  919  poxp  6133  cauappcvgprlemladdrl  7485  caucvgprlemladdrl  7506  xrrebnd  9628  fzpreddisj  9878  fzp1nel  9911  gcdsupex  11673  gcdsupcl  11674  gcdnncl  11683  gcd2n0cl  11685  qredeu  11805  cncongr2  11812  divnumden  11901  divdenle  11902  ivthinclemdisj  12817
  Copyright terms: Public domain W3C validator