Theorem pm2.01da 810

Description: Deduction based on reductio ad absurdum. See pm2.01 190. (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 417	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 192	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 401

This theorem is referenced by:  efrirr  5642  omlimcl  8562  hartogslem1  9503  cfslb2n  10251  fin23lem41  10335  tskuni  10767  4sqlem18  17021  ramlb  17078  ivthlem2  25579  ivthlem3  25580  cosne0  26659  footne  28961  nsnlplig  30773  unbdqndv1  36985  unbdqndv2  36988  knoppndv  37011  dvrelog2b  42722  sticksstones22  42824  fmtno4prm  48215