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  889  nelrdva  3026  ifnefals  3669  exmid01  4313  frirrg  4473  fimax2gtrilemstep  7160  unsnfidcex  7182  unsnfidcel  7183  difinfsn  7393  nninfisollemne  7424  fodju0  7440  nninfwlpoimlemginf  7469  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidapne  7579  ltntri  8406  prodgt0  9131  ixxdisj  10242  icodisj  10331  zsupcllemstep  10596  infssuzex  10600  suprzubdc  10603  iseqf1olemnab  10870  seq3f1olemqsumk  10881  hashtpglem  11226  ltabs  11780  divalglemnqt  12614  bitsfzolem  12648  bitsfzo  12649  sqnprm  12841  ballotfilem2  13153  ballotfilemfc0  13157  ballotfilemfcc  13158  znnen  13170  aprnzr  14459  dedekindeulemuub  15531  dedekindeulemlu  15535  dedekindicclemuub  15540  dedekindicclemlu  15544  ivthinclemlopn  15550  ivthinclemuopn  15552  limcimo  15579  cnplimclemle  15582  pilem3  15697  logbgcd1irraplemexp  15882  mersenne  15914  gausslemma2dlem1f1o  15982  umgrnloop2  16195  pw1ndom3lem  16812  pwtrufal  16820  pwle2  16821  peano3nninf  16834  nninffeq  16847  refeq  16857  trilpolemeq1  16873  taupi  16908