Theorem pm2.01da 458

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

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

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 197  df-an 386

This theorem is referenced by:  efrirr  5095  omlimcl  7658  hartogslem1  8447  cfslb2n  9090  fin23lem41  9174  tskuni  9605  4sqlem18  15666  ramlb  15723  ivthlem2  23221  ivthlem3  23222  cosne0  24276  footne  25615  nsnlplig  27333  unbdqndv1  32499  unbdqndv2  32502  knoppndv  32525  fmtno4prm  41487