Theorem pm2.01da 798

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

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

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 210  df-an 400

This theorem is referenced by:  efrirr  5500  omlimcl  8187  hartogslem1  8990  cfslb2n  9679  fin23lem41  9763  tskuni  10194  4sqlem18  16288  ramlb  16345  ivthlem2  24056  ivthlem3  24057  cosne0  25121  footne  26517  nsnlplig  28264  unbdqndv1  33960  unbdqndv2  33963  knoppndv  33986  fmtno4prm  44092