Theorem pm2.01da 799

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 190	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 207  df-an 396

This theorem is referenced by:  efrirr  5611  omlimcl  8513  hartogslem1  9457  cfslb2n  10190  fin23lem41  10274  tskuni  10706  4sqlem18  16933  ramlb  16990  ivthlem2  25419  ivthlem3  25420  cosne0  26493  footne  28791  nsnlplig  30552  unbdqndv1  36768  unbdqndv2  36771  knoppndv  36794  dvrelog2b  42505  sticksstones22  42607  fmtno4prm  48038