Theorem pm2.01da 457

Description: Deduction based on reductio ad absurdum. (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 449	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 180	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  efrirr  5019  omlimcl  7545  hartogslem1  8330  cfslb2n  8973  fin23lem41  9057  tskuni  9484  4sqlem18  15504  ramlb  15561  ivthlem2  23028  ivthlem3  23029  cosne0  24080  footne  25415  unbdqndv1  31669  unbdqndv2  31672  knoppndv  31695  fmtno4prm  40025