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  8593  hartogslem1  9543  cfslb2n  10353  fin23lem41  10437  tskuni  10875  4sqlem18  17149  ramlb  17206  ivthlem2  25782  ivthlem3  25783  cosne0  26866  footne  29207  nsnlplig  31092  unbdqndv1  37470  unbdqndv2  37473  knoppndv  37496  dvrelog2b  43225  sticksstones22  43327  fmtno4prm  48768