Theorem pm2.65da 650

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

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 114	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 114	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 649	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem is referenced by:  condandc  866  nelrdva  2886  exmid01  4116  frirrg  4267  fimax2gtrilemstep  6787  unsnfidcex  6801  unsnfidcel  6802  difinfsn  6978  fodju0  7012  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  ltntri  7883  prodgt0  8603  ixxdisj  9679  icodisj  9768  iseqf1olemnab  10254  seq3f1olemqsumk  10265  ltabs  10852  divalglemnqt  11606  zsupcllemstep  11627  infssuzex  11631  sqnprm  11805  znnen  11900  dedekindeulemuub  12753  dedekindeulemlu  12757  dedekindicclemuub  12762  dedekindicclemlu  12766  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimo  12792  cnplimclemle  12795  pilem3  12853  pwtrufal  13181  pwle2  13182  peano3nninf  13190  nninffeq  13205  refeq  13212  trilpolemeq1  13222  taupi  13228