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  2971  ifnefals  3604  exmid01  4232  frirrg  4386  fimax2gtrilemstep  6962  unsnfidcex  6982  unsnfidcel  6983  difinfsn  7167  nninfisollemne  7198  fodju0  7214  nninfwlpoimlemginf  7243  exmidfodomrlemr  7271  exmidfodomrlemrALT  7272  exmidapne  7329  ltntri  8156  prodgt0  8881  ixxdisj  9980  icodisj  10069  zsupcllemstep  10321  infssuzex  10325  suprzubdc  10328  iseqf1olemnab  10595  seq3f1olemqsumk  10606  ltabs  11254  divalglemnqt  12087  bitsfzolem  12121  bitsfzo  12122  sqnprm  12314  znnen  12625  dedekindeulemuub  14863  dedekindeulemlu  14867  dedekindicclemuub  14872  dedekindicclemlu  14876  ivthinclemlopn  14882  ivthinclemuopn  14884  limcimo  14911  cnplimclemle  14914  pilem3  15029  logbgcd1irraplemexp  15214  mersenne  15243  gausslemma2dlem1f1o  15311  pwtrufal  15652  pwle2  15653  peano3nninf  15661  nninffeq  15674  refeq  15682  trilpolemeq1  15694  taupi  15727