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  5638  omlimcl  8624  hartogslem1  9573  cfslb2n  10385  fin23lem41  10469  tskuni  10907  4sqlem18  17184  ramlb  17241  ivthlem2  25828  ivthlem3  25829  cosne0  26914  footne  29255  nsnlplig  31140  unbdqndv1  37589  unbdqndv2  37592  knoppndv  37615  dvrelog2b  43382  sticksstones22  43484  fmtno4prm  48933