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 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
StepHypRef Expression
1 pm2.01da.1 . . 3 ((𝜑𝜓) → ¬ 𝜓)
21ex 450 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 181 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
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  5060  omlimcl  7610  hartogslem1  8399  cfslb2n  9042  fin23lem41  9126  tskuni  9557  4sqlem18  15601  ramlb  15658  ivthlem2  23144  ivthlem3  23145  cosne0  24197  footne  25532  n0lpligALT  27206  unbdqndv1  32176  unbdqndv2  32179  knoppndv  32202  fmtno4prm  40812
  Copyright terms: Public domain W3C validator