Theorem pm2.65da 671

Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

Hypotheses

Ref	Expression
pm2.65da.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.65da.2	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)

Assertion

Ref	Expression
pm2.65da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.65da

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 115	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 670	1 ⊢ (𝜑 → ¬ 𝜓)

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 623  ax-in2 624

This theorem is referenced by:  condandc  893  nelrdva  3033  ifnefals  3685  exmid01  4333  frirrg  4493  fimax2gtrilemstep  7199  unsnfidcex  7221  unsnfidcel  7222  difinfsn  7434  nninfisollemne  7465  fodju0  7481  nninfwlpoimlemginf  7510  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidapne  7620  ltntri  8448  prodgt0  9176  ixxdisj  10288  icodisj  10377  zsupcllemstep  10645  infssuzex  10649  suprzubdc  10654  iseqf1olemnab  10921  seq3f1olemqsumk  10932  hashtpglem  11281  sq01  11643  ltabs  11836  divalglemnqt  12670  bitsfzolem  12704  bitsfzo  12705  sqnprm  12897  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemimin  13232  ballotfilemic  13233  ballotfilem1c  13234  znnen  13272  aprnzr  14582  dedekindeulemuub  15701  dedekindeulemlu  15705  dedekindicclemuub  15710  dedekindicclemlu  15714  ivthinclemlopn  15720  ivthinclemuopn  15722  limcimo  15749  cnplimclemle  15752  pilem3  15867  logbgcd1irraplemexp  16053  mersenne  16094  gausslemma2dlem1f1o  16162  umgrnloop2  16375  dichmul0orlem5  16740  dichmul0orlem6  16741  pw1ndom3lem  17002  pwtrufal  17010  pwle2  17011  peano3nninf  17024  nninffeq  17037  refeq  17047  trilpolemeq1  17063  taupi  17097