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  5612  omlimcl  8515  hartogslem1  9459  cfslb2n  10190  fin23lem41  10274  tskuni  10706  4sqlem18  16902  ramlb  16959  ivthlem2  25421  ivthlem3  25422  cosne0  26506  footne  28807  nsnlplig  30568  unbdqndv1  36727  unbdqndv2  36730  knoppndv  36753  dvrelog2b  42433  sticksstones22  42535  fmtno4prm  47932