Theorem pm2.01da 798

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  5604  omlimcl  8505  hartogslem1  9447  cfslb2n  10178  fin23lem41  10262  tskuni  10694  4sqlem18  16890  ramlb  16947  ivthlem2  25409  ivthlem3  25410  cosne0  26494  footne  28795  nsnlplig  30556  unbdqndv1  36708  unbdqndv2  36711  knoppndv  36734  dvrelog2b  42320  sticksstones22  42422  fmtno4prm  47821