Theorem pm2.01da 808

Description: Deduction based on reductio ad absurdum. See pm2.01 189. (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 191	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 209  df-an 400

This theorem is referenced by:  efrirr  5623  omlimcl  8541  hartogslem1  9484  cfslb2n  10219  fin23lem41  10303  tskuni  10735  4sqlem18  16989  ramlb  17046  ivthlem2  25502  ivthlem3  25503  cosne0  26582  footne  28880  nsnlplig  30641  unbdqndv1  36907  unbdqndv2  36910  knoppndv  36933  dvrelog2b  42644  sticksstones22  42746  fmtno4prm  48145