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 797
Description: Deduction based on reductio ad absurdum. See pm2.01 191. (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 415 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 192 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  efrirr  5535  omlimcl  8203  hartogslem1  9005  cfslb2n  9689  fin23lem41  9773  tskuni  10204  4sqlem18  16297  ramlb  16354  ivthlem2  24052  ivthlem3  24053  cosne0  25113  footne  26508  nsnlplig  28257  unbdqndv1  33847  unbdqndv2  33850  knoppndv  33873  fmtno4prm  43736
  Copyright terms: Public domain W3C validator