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 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  efrirr  5640  omlimcl  8561  hartogslem1  9502  cfslb2n  10258  fin23lem41  10342  tskuni  10774  4sqlem18  17028  ramlb  17085  ivthlem2  25622  ivthlem3  25623  cosne0  26705  footne  29014  nsnlplig  30844  unbdqndv1  37125  unbdqndv2  37128  knoppndv  37151  dvrelog2b  42861  sticksstones22  42963  fmtno4prm  48355