Theorem pm2.65da 651

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 650	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 604  ax-in2 605

This theorem is referenced by:  condandc  867  nelrdva  2895  exmid01  4129  frirrg  4280  fimax2gtrilemstep  6802  unsnfidcex  6816  unsnfidcel  6817  difinfsn  6993  fodju0  7027  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  ltntri  7914  prodgt0  8634  ixxdisj  9716  icodisj  9805  iseqf1olemnab  10292  seq3f1olemqsumk  10303  ltabs  10891  divalglemnqt  11653  zsupcllemstep  11674  infssuzex  11678  sqnprm  11852  znnen  11947  dedekindeulemuub  12803  dedekindeulemlu  12807  dedekindicclemuub  12812  dedekindicclemlu  12816  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimo  12842  cnplimclemle  12845  pilem3  12912  logbgcd1irraplemexp  13093  pwtrufal  13365  pwle2  13366  peano3nninf  13376  nninffeq  13391  refeq  13398  trilpolemeq1  13408  taupi  13430