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  3011  ifnefals  3648  exmid01  4286  frirrg  4445  fimax2gtrilemstep  7085  unsnfidcex  7107  unsnfidcel  7108  difinfsn  7293  nninfisollemne  7324  fodju0  7340  nninfwlpoimlemginf  7369  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidapne  7472  ltntri  8300  prodgt0  9025  ixxdisj  10131  icodisj  10220  zsupcllemstep  10482  infssuzex  10486  suprzubdc  10489  iseqf1olemnab  10756  seq3f1olemqsumk  10767  ltabs  11641  divalglemnqt  12474  bitsfzolem  12508  bitsfzo  12509  sqnprm  12701  znnen  13012  dedekindeulemuub  15334  dedekindeulemlu  15338  dedekindicclemuub  15343  dedekindicclemlu  15347  ivthinclemlopn  15353  ivthinclemuopn  15355  limcimo  15382  cnplimclemle  15385  pilem3  15500  logbgcd1irraplemexp  15685  mersenne  15714  gausslemma2dlem1f1o  15782  umgrnloop2  15995  pw1ndom3lem  16538  pwtrufal  16548  pwle2  16549  peano3nninf  16559  nninffeq  16572  refeq  16582  trilpolemeq1  16594  taupi  16627