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  3010  ifnefals  3647  exmid01  4283  frirrg  4442  fimax2gtrilemstep  7076  unsnfidcex  7098  unsnfidcel  7099  difinfsn  7283  nninfisollemne  7314  fodju0  7330  nninfwlpoimlemginf  7359  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidapne  7462  ltntri  8290  prodgt0  9015  ixxdisj  10116  icodisj  10205  zsupcllemstep  10466  infssuzex  10470  suprzubdc  10473  iseqf1olemnab  10740  seq3f1olemqsumk  10751  ltabs  11619  divalglemnqt  12452  bitsfzolem  12486  bitsfzo  12487  sqnprm  12679  znnen  12990  dedekindeulemuub  15312  dedekindeulemlu  15316  dedekindicclemuub  15321  dedekindicclemlu  15325  ivthinclemlopn  15331  ivthinclemuopn  15333  limcimo  15360  cnplimclemle  15363  pilem3  15478  logbgcd1irraplemexp  15663  mersenne  15692  gausslemma2dlem1f1o  15760  umgrnloop2  15970  pw1ndom3lem  16466  pwtrufal  16476  pwle2  16477  peano3nninf  16487  nninffeq  16500  refeq  16510  trilpolemeq1  16522  taupi  16555