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  5603  omlimcl  8503  hartogslem1  9453  cfslb2n  10181  fin23lem41  10265  tskuni  10696  4sqlem18  16892  ramlb  16949  ivthlem2  25369  ivthlem3  25370  cosne0  26454  footne  28686  nsnlplig  30443  unbdqndv1  36484  unbdqndv2  36487  knoppndv  36510  dvrelog2b  42042  sticksstones22  42144  fmtno4prm  47563