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 798
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 414 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397
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 398
This theorem is referenced by:  efrirr  5658  omlimcl  8578  hartogslem1  9537  cfslb2n  10263  fin23lem41  10347  tskuni  10778  4sqlem18  16895  ramlb  16952  ivthlem2  24969  ivthlem3  24970  cosne0  26038  footne  27974  nsnlplig  29734  unbdqndv1  35384  unbdqndv2  35387  knoppndv  35410  dvrelog2b  40931  sticksstones22  40984  fmtno4prm  46243
  Copyright terms: Public domain W3C validator