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

Theorem pm2.65da 623
Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
Hypotheses
Ref Expression
pm2.65da.1  |-  ( (
ph  /\  ps )  ->  ch )
pm2.65da.2  |-  ( (
ph  /\  ps )  ->  -.  ch )
Assertion
Ref Expression
pm2.65da  |-  ( ph  ->  -.  ps )

Proof of Theorem pm2.65da
StepHypRef Expression
1 pm2.65da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 114 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 114 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 622 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107  ax-in1 580  ax-in2 581
This theorem is referenced by:  condandc  814  nelrdva  2823  exmid01  4038  frirrg  4186  fimax2gtrilemstep  6670  unsnfidcex  6684  unsnfidcel  6685  fodjuomnilem0  6863  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  prodgt0  8374  ixxdisj  9382  icodisj  9470  iseqf1olemnab  9978  seq3f1olemqsumk  9989  ltabs  10581  divalglemnqt  11259  zsupcllemstep  11280  infssuzex  11284  sqnprm  11456  znnen  11550  peano3nninf  12169
  Copyright terms: Public domain W3C validator