Theorem pm2.65da 662

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 661	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 615  ax-in2 616

This theorem is referenced by:  condandc  882  nelrdva  2956  exmid01  4210  frirrg  4362  fimax2gtrilemstep  6914  unsnfidcex  6933  unsnfidcel  6934  difinfsn  7113  nninfisollemne  7143  fodju0  7159  nninfwlpoimlemginf  7188  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  exmidapne  7273  ltntri  8099  prodgt0  8823  ixxdisj  9917  icodisj  10006  iseqf1olemnab  10502  seq3f1olemqsumk  10513  ltabs  11110  divalglemnqt  11939  zsupcllemstep  11960  infssuzex  11964  suprzubdc  11967  sqnprm  12150  znnen  12413  dedekindeulemuub  14448  dedekindeulemlu  14452  dedekindicclemuub  14457  dedekindicclemlu  14461  ivthinclemlopn  14467  ivthinclemuopn  14469  limcimo  14487  cnplimclemle  14490  pilem3  14557  logbgcd1irraplemexp  14739  pwtrufal  15101  pwle2  15102  peano3nninf  15110  nninffeq  15123  refeq  15130  trilpolemeq1  15142  taupi  15175