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  5635  omlimcl  8565  hartogslem1  9514  cfslb2n  10270  fin23lem41  10354  tskuni  10792  4sqlem18  17054  ramlb  17111  ivthlem2  25680  ivthlem3  25681  cosne0  26766  footne  29077  nsnlplig  30962  unbdqndv1  37205  unbdqndv2  37208  knoppndv  37231  dvrelog2b  42932  sticksstones22  43034  fmtno4prm  48478