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

Theorem pm2.65da 661
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 115 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 115 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 660 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 614  ax-in2 615
This theorem is referenced by:  condandc  881  nelrdva  2944  exmid01  4195  frirrg  4346  fimax2gtrilemstep  6893  unsnfidcex  6912  unsnfidcel  6913  difinfsn  7092  nninfisollemne  7122  fodju0  7138  nninfwlpoimlemginf  7167  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  ltntri  8062  prodgt0  8785  ixxdisj  9877  icodisj  9966  iseqf1olemnab  10461  seq3f1olemqsumk  10472  ltabs  11067  divalglemnqt  11895  zsupcllemstep  11916  infssuzex  11920  suprzubdc  11923  sqnprm  12106  znnen  12369  dedekindeulemuub  13728  dedekindeulemlu  13732  dedekindicclemuub  13737  dedekindicclemlu  13741  ivthinclemlopn  13747  ivthinclemuopn  13749  limcimo  13767  cnplimclemle  13770  pilem3  13837  logbgcd1irraplemexp  14019  pwtrufal  14369  pwle2  14370  peano3nninf  14379  nninffeq  14392  refeq  14399  trilpolemeq1  14411  taupi  14441
  Copyright terms: Public domain W3C validator