Theorem pm2.65da 663

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 662	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  883  nelrdva  2981  ifnefals  3615  exmid01  4246  frirrg  4401  fimax2gtrilemstep  7004  unsnfidcex  7024  unsnfidcel  7025  difinfsn  7209  nninfisollemne  7240  fodju0  7256  nninfwlpoimlemginf  7285  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  exmidapne  7379  ltntri  8207  prodgt0  8932  ixxdisj  10032  icodisj  10121  zsupcllemstep  10379  infssuzex  10383  suprzubdc  10386  iseqf1olemnab  10653  seq3f1olemqsumk  10664  ltabs  11442  divalglemnqt  12275  bitsfzolem  12309  bitsfzo  12310  sqnprm  12502  znnen  12813  dedekindeulemuub  15133  dedekindeulemlu  15137  dedekindicclemuub  15142  dedekindicclemlu  15146  ivthinclemlopn  15152  ivthinclemuopn  15154  limcimo  15181  cnplimclemle  15184  pilem3  15299  logbgcd1irraplemexp  15484  mersenne  15513  gausslemma2dlem1f1o  15581  pwtrufal  16008  pwle2  16009  peano3nninf  16018  nninffeq  16031  refeq  16041  trilpolemeq1  16053  taupi  16086