Theorem pm2.01da 799

Description: Deduction based on reductio ad absurdum. See pm2.01 192. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypothesis

Ref	Expression
pm2.01da.1	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)

Assertion

Ref	Expression
pm2.01da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.01da

Step	Hyp	Ref	Expression
1		pm2.01da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓)
2	1	ex 416	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 193	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  efrirr  5506  omlimcl  8235  hartogslem1  9079  cfslb2n  9768  fin23lem41  9852  tskuni  10283  4sqlem18  16398  ramlb  16455  ivthlem2  24204  ivthlem3  24205  cosne0  25273  footne  26669  nsnlplig  28416  unbdqndv1  34326  unbdqndv2  34329  knoppndv  34352  dvrelog2b  39693  fmtno4prm  44561