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  7211  unsnfidcex  7233  unsnfidcel  7234  difinfsn  7447  nninfisollemne  7478  fodju0  7494  nninfwlpoimlemginf  7523  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidapne  7633  ltntri  8462  prodgt0  9191  ixxdisj  10322  icodisj  10411  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  iseqf1olemnab  10959  seq3f1olemqsumk  10970  hashtpglem  11320  sq01  11682  ltabs  11876  divalglemnqt  12712  bitsfzolem  12746  bitsfzo  12747  sqnprm  12940  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  ballotfilemic  13308  ballotfilem1c  13309  znnen  13347  aprnzr  14708  psrbagfsuppub  15192  mplsubrglemcl  15249  dedekindeulemuub  15876  dedekindeulemlu  15880  dedekindicclemuub  15885  dedekindicclemlu  15889  ivthinclemlopn  15895  ivthinclemuopn  15897  limcimo  15924  cnplimclemle  15927  pilem3  16043  logbgcd1irraplemexp  16237  mersenne  16330  bpos  16353  gausslemma2dlem1f1o  16417  umgrnloop2  16630  dichmul0orlem5  16995  dichmul0orlem6  16996  pw1ndom3lem  17257  pwtrufal  17265  pwle2  17266  peano3nninf  17289  nninffeq  17302  refeq  17312  trilpolemeq1  17329  taupi  17363