Theorem pm2.01da 810

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

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

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 210  df-an 401

This theorem is referenced by:  efrirr  5641  omlimcl  8559  hartogslem1  9500  cfslb2n  10247  fin23lem41  10331  tskuni  10763  4sqlem18  17017  ramlb  17074  ivthlem2  25611  ivthlem3  25612  cosne0  26694  footne  29003  nsnlplig  30833  unbdqndv1  37097  unbdqndv2  37100  knoppndv  37123  dvrelog2b  42833  sticksstones22  42935  fmtno4prm  48327