Theorem pm2.01da 797

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

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

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 398

This theorem is referenced by:  efrirr  5581  omlimcl  8440  hartogslem1  9345  cfslb2n  10070  fin23lem41  10154  tskuni  10585  4sqlem18  16708  ramlb  16765  ivthlem2  24661  ivthlem3  24662  cosne0  25730  footne  27129  nsnlplig  28888  unbdqndv1  34733  unbdqndv2  34736  knoppndv  34759  dvrelog2b  40116  sticksstones22  40166  fmtno4prm  45085