Theorem pm2.65da 671

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 670	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is used by:  condandc  893  nelrdva  3033  ifnefals  3685  exmid01  4337  frirrg  4497  fimax2gtrilemstep  7210  unsnfidcex  7232  unsnfidcel  7233  difinfsn  7447  nninfisollemne  7478  fodju0  7494  nninfwlpoimlemginf  7523  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidapne  7633  ltntri  8462  prodgt0  9191  ixxdisj  10323  icodisj  10412  zsupcllemstep  10680  infssuzex  10684  suprzubdc  10689  iseqf1olemnab  10960  seq3f1olemqsumk  10971  hashtpglem  11321  sq01  11683  ltabs  11877  divalglemnqt  12713  bitsfzolem  12747  bitsfzo  12748  sqnprm  12941  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemimin  13308  ballotfilemic  13309  ballotfilem1c  13310  znnen  13348  aprnzr  14709  dedekindeulemuub  15855  dedekindeulemlu  15859  dedekindicclemuub  15864  dedekindicclemlu  15868  ivthinclemlopn  15874  ivthinclemuopn  15876  limcimo  15903  cnplimclemle  15906  pilem3  16022  logbgcd1irraplemexp  16216  mersenne  16309  bpos  16332  gausslemma2dlem1f1o  16396  umgrnloop2  16609  dichmul0orlem5  16974  dichmul0orlem6  16975  pw1ndom3lem  17236  pwtrufal  17244  pwle2  17245  peano3nninf  17268  nninffeq  17281  refeq  17291  trilpolemeq1  17308  taupi  17342