Theorem pm2.01da 811

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 418	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 192	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  efrirr  5631  omlimcl  8579  hartogslem1  9529  cfslb2n  10339  fin23lem41  10423  tskuni  10861  4sqlem18  17133  ramlb  17190  ivthlem2  25766  ivthlem3  25767  cosne0  26850  footne  29191  nsnlplig  31076  unbdqndv1  37354  unbdqndv2  37357  knoppndv  37380  dvrelog2b  43096  sticksstones22  43198  fmtno4prm  48629