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 792
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 397 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 181 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 383
This theorem is referenced by:  efrirr  5230  omlimcl  7811  hartogslem1  8602  cfslb2n  9291  fin23lem41  9375  tskuni  9806  4sqlem18  15872  ramlb  15929  ivthlem2  23439  ivthlem3  23440  cosne0  24496  footne  25835  nsnlplig  27669  unbdqndv1  32830  unbdqndv2  32833  knoppndv  32856  fmtno4prm  42005
  Copyright terms: Public domain W3C validator