Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbi Structured version   Visualization version   GIF version

Theorem mtbi 326
 Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mtbi.1 ¬ 𝜑
mtbi.2 (𝜑𝜓)
Assertion
Ref Expression
mtbi ¬ 𝜓

Proof of Theorem mtbi
StepHypRef Expression
1 mtbi.1 . 2 ¬ 𝜑
2 mtbi.2 . . 3 (𝜑𝜓)
32biimpri 231 . 2 (𝜓𝜑)
41, 3mto 200 1 ¬ 𝜓
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209 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 210 This theorem is referenced by:  mtbir  327  vn0  4238  vnex  5185  opthwiener  5374  epelg  5437  harndom  9060  alephprc  9560  unialeph  9562  ndvdsi  15814  nprmi  16086  dec2dvds  16455  dec5dvds2  16457  mreexmrid  16973  sinhalfpilem  25156  ppi2i  25854  axlowdimlem13  26848  ex-mod  28334  measvuni  31702  ballotlem2  31975  sgnmulsgp  32037  bnj1224  32302  bnj1541  32357  bnj1311  32525  dfon2lem7  33282  onsucsuccmpi  34182  bj-imn3ani  34316  bj-0nelmpt  34812  bj-pinftynminfty  34923  poimirlem30  35368  clsk1indlem4  41121  alimp-no-surprise  45701
 Copyright terms: Public domain W3C validator