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  886  nelrdva  3010  ifnefals  3647  exmid01  4282  frirrg  4441  fimax2gtrilemstep  7070  unsnfidcex  7090  unsnfidcel  7091  difinfsn  7275  nninfisollemne  7306  fodju0  7322  nninfwlpoimlemginf  7351  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidapne  7454  ltntri  8282  prodgt0  9007  ixxdisj  10107  icodisj  10196  zsupcllemstep  10457  infssuzex  10461  suprzubdc  10464  iseqf1olemnab  10731  seq3f1olemqsumk  10742  ltabs  11606  divalglemnqt  12439  bitsfzolem  12473  bitsfzo  12474  sqnprm  12666  znnen  12977  dedekindeulemuub  15299  dedekindeulemlu  15303  dedekindicclemuub  15308  dedekindicclemlu  15312  ivthinclemlopn  15318  ivthinclemuopn  15320  limcimo  15347  cnplimclemle  15350  pilem3  15465  logbgcd1irraplemexp  15650  mersenne  15679  gausslemma2dlem1f1o  15747  umgrnloop2  15957  pw1ndom3lem  16382  pwtrufal  16392  pwle2  16393  peano3nninf  16403  nninffeq  16416  refeq  16426  trilpolemeq1  16438  taupi  16471