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  889  nelrdva  3023  ifnefals  3666  exmid01  4310  frirrg  4470  fimax2gtrilemstep  7157  unsnfidcex  7179  unsnfidcel  7180  difinfsn  7390  nninfisollemne  7421  fodju0  7437  nninfwlpoimlemginf  7466  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidapne  7570  ltntri  8397  prodgt0  9122  ixxdisj  10232  icodisj  10321  zsupcllemstep  10585  infssuzex  10589  suprzubdc  10592  iseqf1olemnab  10859  seq3f1olemqsumk  10870  hashtpglem  11211  ltabs  11765  divalglemnqt  12599  bitsfzolem  12633  bitsfzo  12634  sqnprm  12826  znnen  13138  dedekindeulemuub  15469  dedekindeulemlu  15473  dedekindicclemuub  15478  dedekindicclemlu  15482  ivthinclemlopn  15488  ivthinclemuopn  15490  limcimo  15517  cnplimclemle  15520  pilem3  15635  logbgcd1irraplemexp  15820  mersenne  15852  gausslemma2dlem1f1o  15920  umgrnloop2  16133  pw1ndom3lem  16750  pwtrufal  16758  pwle2  16759  peano3nninf  16772  nninffeq  16785  refeq  16795  trilpolemeq1  16811  taupi  16845