Theorem pm2.01da 798

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

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

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 207  df-an 396

This theorem is referenced by:  efrirr  5680  omlimcl  8634  hartogslem1  9611  cfslb2n  10337  fin23lem41  10421  tskuni  10852  4sqlem18  17009  ramlb  17066  ivthlem2  25506  ivthlem3  25507  cosne0  26589  footne  28749  nsnlplig  30513  unbdqndv1  36474  unbdqndv2  36477  knoppndv  36500  dvrelog2b  42023  sticksstones22  42125  fmtno4prm  47449