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 795
Description: Deduction based on reductio ad absurdum. See pm2.01 188. (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 411 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  efrirr  5656  omlimcl  8580  hartogslem1  9539  cfslb2n  10265  fin23lem41  10349  tskuni  10780  4sqlem18  16899  ramlb  16956  ivthlem2  25201  ivthlem3  25202  cosne0  26274  footne  28241  nsnlplig  30001  unbdqndv1  35687  unbdqndv2  35690  knoppndv  35713  dvrelog2b  41237  sticksstones22  41290  fmtno4prm  46541
  Copyright terms: Public domain W3C validator