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  2967  ifnefals  3599  exmid01  4227  frirrg  4381  fimax2gtrilemstep  6956  unsnfidcex  6976  unsnfidcel  6977  difinfsn  7159  nninfisollemne  7190  fodju0  7206  nninfwlpoimlemginf  7235  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidapne  7320  ltntri  8147  prodgt0  8871  ixxdisj  9969  icodisj  10058  iseqf1olemnab  10572  seq3f1olemqsumk  10583  ltabs  11231  divalglemnqt  12061  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  sqnprm  12274  znnen  12555  dedekindeulemuub  14771  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemlu  14784  ivthinclemlopn  14790  ivthinclemuopn  14792  limcimo  14819  cnplimclemle  14822  pilem3  14918  logbgcd1irraplemexp  15100  gausslemma2dlem1f1o  15176  pwtrufal  15488  pwle2  15489  peano3nninf  15497  nninffeq  15510  refeq  15518  trilpolemeq1  15530  taupi  15563