MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.01da Structured version   Visualization version   GIF version

Theorem pm2.01da 810
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
StepHypRef Expression
1 pm2.01da.1 . . 3 ((𝜑𝜓) → ¬ 𝜓)
21ex 417 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 192 1 (𝜑 → ¬ 𝜓)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3  wi 4  wa 400
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 401
This theorem is used by:  efrirr  5640  omlimcl  8561  hartogslem1  9502  cfslb2n  10258  fin23lem41  10342  tskuni  10774  4sqlem18  17028  ramlb  17085  ivthlem2  25622  ivthlem3  25623  cosne0  26705  footne  29014  nsnlplig  30844  unbdqndv1  37125  unbdqndv2  37128  knoppndv  37151  dvrelog2b  42861  sticksstones22  42963  fmtno4prm  48355
  Copyright terms: Public domain W3C validator