Theorem pm2.65da 623

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 622	1 |- ( ph -> -. ps )

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

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

This theorem is referenced by:  condandc  814  nelrdva  2823  exmid01  4038  frirrg  4186  fimax2gtrilemstep  6670  unsnfidcex  6684  unsnfidcel  6685  fodjuomnilem0  6863  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  prodgt0  8374  ixxdisj  9382  icodisj  9470  iseqf1olemnab  9978  seq3f1olemqsumk  9989  ltabs  10581  divalglemnqt  11259  zsupcllemstep  11280  infssuzex  11284  sqnprm  11456  znnen  11550  peano3nninf  12169