Theorem pm2.01da 795

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

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

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 206  df-an 396

This theorem is referenced by:  efrirr  5569  omlimcl  8385  hartogslem1  9262  cfslb2n  10008  fin23lem41  10092  tskuni  10523  4sqlem18  16644  ramlb  16701  ivthlem2  24597  ivthlem3  24598  cosne0  25666  footne  27065  nsnlplig  28822  unbdqndv1  34667  unbdqndv2  34670  knoppndv  34693  dvrelog2b  40054  sticksstones22  40104  fmtno4prm  44979