Theorem pm2.65da 662

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 661	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 615  ax-in2 616

This theorem is referenced by:  condandc  882  nelrdva  2971  ifnefals  3604  exmid01  4232  frirrg  4386  fimax2gtrilemstep  6970  unsnfidcex  6990  unsnfidcel  6991  difinfsn  7175  nninfisollemne  7206  fodju0  7222  nninfwlpoimlemginf  7251  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidapne  7345  ltntri  8173  prodgt0  8898  ixxdisj  9997  icodisj  10086  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  iseqf1olemnab  10612  seq3f1olemqsumk  10623  ltabs  11271  divalglemnqt  12104  bitsfzolem  12138  bitsfzo  12139  sqnprm  12331  znnen  12642  dedekindeulemuub  14939  dedekindeulemlu  14943  dedekindicclemuub  14948  dedekindicclemlu  14952  ivthinclemlopn  14958  ivthinclemuopn  14960  limcimo  14987  cnplimclemle  14990  pilem3  15105  logbgcd1irraplemexp  15290  mersenne  15319  gausslemma2dlem1f1o  15387  pwtrufal  15730  pwle2  15731  peano3nninf  15740  nninffeq  15753  refeq  15763  trilpolemeq1  15775  taupi  15808