Theorem pm2.65da 656

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 655	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 609  ax-in2 610

This theorem is referenced by:  condandc  876  nelrdva  2937  exmid01  4184  frirrg  4335  fimax2gtrilemstep  6878  unsnfidcex  6897  unsnfidcel  6898  difinfsn  7077  nninfisollemne  7107  fodju0  7123  nninfwlpoimlemginf  7152  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  ltntri  8047  prodgt0  8768  ixxdisj  9860  icodisj  9949  iseqf1olemnab  10444  seq3f1olemqsumk  10455  ltabs  11051  divalglemnqt  11879  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  sqnprm  12090  znnen  12353  dedekindeulemuub  13389  dedekindeulemlu  13393  dedekindicclemuub  13398  dedekindicclemlu  13402  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimo  13428  cnplimclemle  13431  pilem3  13498  logbgcd1irraplemexp  13680  pwtrufal  14030  pwle2  14031  peano3nninf  14040  nninffeq  14053  refeq  14060  trilpolemeq1  14072  taupi  14102