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 799
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 412 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
32pm2.01d 190 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  efrirr  5665  omlimcl  8616  hartogslem1  9582  cfslb2n  10308  fin23lem41  10392  tskuni  10823  4sqlem18  17000  ramlb  17057  ivthlem2  25487  ivthlem3  25488  cosne0  26571  footne  28731  nsnlplig  30500  unbdqndv1  36509  unbdqndv2  36512  knoppndv  36535  dvrelog2b  42067  sticksstones22  42169  fmtno4prm  47562
  Copyright terms: Public domain W3C validator