Theorem pm2.65da 650

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 114	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 114	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 649	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem is referenced by:  condandc  866  nelrdva  2891  exmid01  4121  frirrg  4272  fimax2gtrilemstep  6794  unsnfidcex  6808  unsnfidcel  6809  difinfsn  6985  fodju0  7019  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  ltntri  7890  prodgt0  8610  ixxdisj  9686  icodisj  9775  iseqf1olemnab  10261  seq3f1olemqsumk  10272  ltabs  10859  divalglemnqt  11617  zsupcllemstep  11638  infssuzex  11642  sqnprm  11816  znnen  11911  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimo  12803  cnplimclemle  12806  pilem3  12864  pwtrufal  13192  pwle2  13193  peano3nninf  13201  nninffeq  13216  refeq  13223  trilpolemeq1  13233  taupi  13239