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  4335  frirrg  4495  fimax2gtrilemstep  7205  unsnfidcex  7227  unsnfidcel  7228  difinfsn  7440  nninfisollemne  7471  fodju0  7487  nninfwlpoimlemginf  7516  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidapne  7626  ltntri  8454  prodgt0  9183  ixxdisj  10307  icodisj  10396  zsupcllemstep  10664  infssuzex  10668  suprzubdc  10673  iseqf1olemnab  10940  seq3f1olemqsumk  10951  hashtpglem  11300  sq01  11662  ltabs  11855  divalglemnqt  12689  bitsfzolem  12723  bitsfzo  12724  sqnprm  12916  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemimin  13251  ballotfilemic  13252  ballotfilem1c  13253  znnen  13291  aprnzr  14601  dedekindeulemuub  15720  dedekindeulemlu  15724  dedekindicclemuub  15729  dedekindicclemlu  15733  ivthinclemlopn  15739  ivthinclemuopn  15741  limcimo  15768  cnplimclemle  15771  pilem3  15887  logbgcd1irraplemexp  16076  mersenne  16117  gausslemma2dlem1f1o  16191  umgrnloop2  16404  dichmul0orlem5  16769  dichmul0orlem6  16770  pw1ndom3lem  17031  pwtrufal  17039  pwle2  17040  peano3nninf  17062  nninffeq  17075  refeq  17085  trilpolemeq1  17101  taupi  17135