Theorem pm2.65da 665

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 664	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 617  ax-in2 618

This theorem is referenced by:  condandc  885  nelrdva  2990  ifnefals  3627  exmid01  4261  frirrg  4418  fimax2gtrilemstep  7030  unsnfidcex  7050  unsnfidcel  7051  difinfsn  7235  nninfisollemne  7266  fodju0  7282  nninfwlpoimlemginf  7311  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  exmidapne  7414  ltntri  8242  prodgt0  8967  ixxdisj  10067  icodisj  10156  zsupcllemstep  10416  infssuzex  10420  suprzubdc  10423  iseqf1olemnab  10690  seq3f1olemqsumk  10701  ltabs  11564  divalglemnqt  12397  bitsfzolem  12431  bitsfzo  12432  sqnprm  12624  znnen  12935  dedekindeulemuub  15256  dedekindeulemlu  15260  dedekindicclemuub  15265  dedekindicclemlu  15269  ivthinclemlopn  15275  ivthinclemuopn  15277  limcimo  15304  cnplimclemle  15307  pilem3  15422  logbgcd1irraplemexp  15607  mersenne  15636  gausslemma2dlem1f1o  15704  umgrnloop2  15914  pwtrufal  16274  pwle2  16275  peano3nninf  16284  nninffeq  16297  refeq  16307  trilpolemeq1  16319  taupi  16352