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  3013  ifnefals  3650  exmid01  4288  frirrg  4447  fimax2gtrilemstep  7090  unsnfidcex  7112  unsnfidcel  7113  difinfsn  7299  nninfisollemne  7330  fodju0  7346  nninfwlpoimlemginf  7375  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidapne  7479  ltntri  8307  prodgt0  9032  ixxdisj  10138  icodisj  10227  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  iseqf1olemnab  10764  seq3f1olemqsumk  10775  ltabs  11649  divalglemnqt  12483  bitsfzolem  12517  bitsfzo  12518  sqnprm  12710  znnen  13021  dedekindeulemuub  15344  dedekindeulemlu  15348  dedekindicclemuub  15353  dedekindicclemlu  15357  ivthinclemlopn  15363  ivthinclemuopn  15365  limcimo  15392  cnplimclemle  15395  pilem3  15510  logbgcd1irraplemexp  15695  mersenne  15724  gausslemma2dlem1f1o  15792  umgrnloop2  16005  pw1ndom3lem  16609  pwtrufal  16619  pwle2  16620  peano3nninf  16630  nninffeq  16643  refeq  16653  trilpolemeq1  16665  taupi  16698