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  2919  exmid01  4159  frirrg  4310  fimax2gtrilemstep  6845  unsnfidcex  6864  unsnfidcel  6865  difinfsn  7044  nninfisollemne  7074  fodju0  7090  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  ltntri  8003  prodgt0  8723  ixxdisj  9807  icodisj  9896  iseqf1olemnab  10387  seq3f1olemqsumk  10398  ltabs  10987  divalglemnqt  11810  zsupcllemstep  11831  infssuzex  11835  sqnprm  12012  znnen  12127  dedekindeulemuub  12995  dedekindeulemlu  12999  dedekindicclemuub  13004  dedekindicclemlu  13008  ivthinclemlopn  13014  ivthinclemuopn  13016  limcimo  13034  cnplimclemle  13037  pilem3  13104  logbgcd1irraplemexp  13285  pwtrufal  13569  pwle2  13570  peano3nninf  13579  nninffeq  13592  refeq  13599  trilpolemeq1  13611  taupi  13641