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  5591  omlimcl  8488  hartogslem1  9423  cfslb2n  10154  fin23lem41  10238  tskuni  10669  4sqlem18  16869  ramlb  16926  ivthlem2  25375  ivthlem3  25376  cosne0  26460  footne  28696  nsnlplig  30453  unbdqndv1  36542  unbdqndv2  36545  knoppndv  36568  dvrelog2b  42099  sticksstones22  42201  fmtno4prm  47606