Theorem pm2.65da 665

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 617  ax-in2 618

This theorem is referenced by:  condandc  886  nelrdva  3011  ifnefals  3648  exmid01  4286  frirrg  4445  fimax2gtrilemstep  7083  unsnfidcex  7105  unsnfidcel  7106  difinfsn  7290  nninfisollemne  7321  fodju0  7337  nninfwlpoimlemginf  7366  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidapne  7469  ltntri  8297  prodgt0  9022  ixxdisj  10128  icodisj  10217  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  iseqf1olemnab  10753  seq3f1olemqsumk  10764  ltabs  11638  divalglemnqt  12471  bitsfzolem  12505  bitsfzo  12506  sqnprm  12698  znnen  13009  dedekindeulemuub  15331  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemlu  15344  ivthinclemlopn  15350  ivthinclemuopn  15352  limcimo  15379  cnplimclemle  15382  pilem3  15497  logbgcd1irraplemexp  15682  mersenne  15711  gausslemma2dlem1f1o  15779  umgrnloop2  15990  pw1ndom3lem  16524  pwtrufal  16534  pwle2  16535  peano3nninf  16545  nninffeq  16558  refeq  16568  trilpolemeq1  16580  taupi  16613