Theorem pm2.65da 667

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 666	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 619  ax-in2 620

This theorem is referenced by:  condandc  889  nelrdva  3027  ifnefals  3671  exmid01  4316  frirrg  4476  fimax2gtrilemstep  7171  unsnfidcex  7193  unsnfidcel  7194  difinfsn  7404  nninfisollemne  7435  fodju0  7451  nninfwlpoimlemginf  7480  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidapne  7590  ltntri  8418  prodgt0  9146  ixxdisj  10258  icodisj  10347  zsupcllemstep  10614  infssuzex  10618  suprzubdc  10623  iseqf1olemnab  10890  seq3f1olemqsumk  10901  hashtpglem  11246  ltabs  11800  divalglemnqt  12634  bitsfzolem  12668  bitsfzo  12669  sqnprm  12861  ballotfilem2  13175  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemimin  13196  ballotfilemic  13197  ballotfilem1c  13198  znnen  13236  aprnzr  14540  dedekindeulemuub  15611  dedekindeulemlu  15615  dedekindicclemuub  15620  dedekindicclemlu  15624  ivthinclemlopn  15630  ivthinclemuopn  15632  limcimo  15659  cnplimclemle  15662  pilem3  15777  logbgcd1irraplemexp  15962  mersenne  15994  gausslemma2dlem1f1o  16062  umgrnloop2  16275  dichmul0orlem5  16640  dichmul0orlem6  16641  pw1ndom3lem  16902  pwtrufal  16910  pwle2  16911  peano3nninf  16924  nninffeq  16937  refeq  16947  trilpolemeq1  16963  taupi  16998