Theorem pm2.65da 667

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 666	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 619  ax-in2 620

This theorem is referenced by:  condandc  888  nelrdva  3012  ifnefals  3651  exmid01  4290  frirrg  4449  fimax2gtrilemstep  7095  unsnfidcex  7117  unsnfidcel  7118  difinfsn  7304  nninfisollemne  7335  fodju0  7351  nninfwlpoimlemginf  7380  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  exmidapne  7484  ltntri  8312  prodgt0  9037  ixxdisj  10143  icodisj  10232  zsupcllemstep  10495  infssuzex  10499  suprzubdc  10502  iseqf1olemnab  10769  seq3f1olemqsumk  10780  hashtpglem  11116  ltabs  11670  divalglemnqt  12504  bitsfzolem  12538  bitsfzo  12539  sqnprm  12731  znnen  13042  dedekindeulemuub  15370  dedekindeulemlu  15374  dedekindicclemuub  15379  dedekindicclemlu  15383  ivthinclemlopn  15389  ivthinclemuopn  15391  limcimo  15418  cnplimclemle  15421  pilem3  15536  logbgcd1irraplemexp  15721  mersenne  15750  gausslemma2dlem1f1o  15818  umgrnloop2  16031  pw1ndom3lem  16648  pwtrufal  16658  pwle2  16659  peano3nninf  16672  nninffeq  16685  refeq  16695  trilpolemeq1  16711  taupi  16745