Theorem pm2.01da 811

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 418	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
3	2	pm2.01d 192	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 402

This theorem is used by:  efrirr  5643  omlimcl  8569  hartogslem1  9511  cfslb2n  10267  fin23lem41  10351  tskuni  10783  4sqlem18  17044  ramlb  17101  ivthlem2  25662  ivthlem3  25663  cosne0  26745  footne  29054  nsnlplig  30904  unbdqndv1  37154  unbdqndv2  37157  knoppndv  37180  dvrelog2b  42891  sticksstones22  42993  fmtno4prm  48385