Theorem pm2.65da 622

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 113	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 113	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 621	1 |- ( ph -> -. ps )

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

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

This theorem is referenced by:  condandc  813  nelrdva  2822  exmid01  4032  frirrg  4177  fimax2gtrilemstep  6616  unsnfidcex  6630  unsnfidcel  6631  fodjuomnilem0  6802  exmidfodomrlemr  6828  exmidfodomrlemrALT  6829  prodgt0  8313  ixxdisj  9321  icodisj  9409  iseqf1olemnab  9917  seq3f1olemqsumk  9928  ltabs  10520  divalglemnqt  11198  zsupcllemstep  11219  infssuzex  11223  sqnprm  11395  znnen  11489  peano3nninf  11897