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

Theorem mtbi 311
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 218 . 2 (𝜓𝜑)
41, 3mto 188 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  mtbir  312  vprc  4829  vnex  4831  opthwiener  5005  harndom  8510  alephprc  8960  unialeph  8962  ndvdsi  15183  bitsfzo  15204  nprmi  15449  dec2dvds  15814  dec5dvds2  15816  mreexmrid  16350  sinhalfpilem  24260  ppi2i  24940  axlowdimlem13  25879  ex-mod  27436  measvuni  30405  ballotlem2  30678  sgnmulsgp  30740  bnj1224  30998  bnj1541  31052  bnj1311  31218  dfon2lem7  31818  onsucsuccmpi  32567  bj-imn3ani  32697  bj-0nelmpt  33194  bj-pinftynminfty  33244  poimirlem30  33569  clsk1indlem4  38659  alimp-no-surprise  42855
  Copyright terms: Public domain W3C validator