Theorem pm2.01da 796

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

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

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 206  df-an 396

This theorem is referenced by:  efrirr  5648  omlimcl  8574  hartogslem1  9534  cfslb2n  10260  fin23lem41  10344  tskuni  10775  4sqlem18  16896  ramlb  16953  ivthlem2  25305  ivthlem3  25306  cosne0  26382  footne  28446  nsnlplig  30206  unbdqndv1  35875  unbdqndv2  35878  knoppndv  35901  dvrelog2b  41428  sticksstones22  41481  fmtno4prm  46753