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

Theorem pm2.65da 622
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 113 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 113 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 621 1  |-  ( ph  ->  -.  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-ia3 106  ax-in1 579  ax-in2 580
This theorem is referenced by:  condandc  813  nelrdva  2822  exmid01  4032  frirrg  4177  fimax2gtrilemstep  6616  unsnfidcex  6630  unsnfidcel  6631  fodjuomnilem0  6802  exmidfodomrlemr  6828  exmidfodomrlemrALT  6829  prodgt0  8313  ixxdisj  9321  icodisj  9409  iseqf1olemnab  9917  seq3f1olemqsumk  9928  ltabs  10520  divalglemnqt  11198  zsupcllemstep  11219  infssuzex  11223  sqnprm  11395  znnen  11489  peano3nninf  11897
  Copyright terms: Public domain W3C validator