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

Theorem mtbi 313
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 219 . 2 (𝜓𝜑)
41, 3mto 188 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197
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 198
This theorem is referenced by:  mtbir  314  vnex  4959  opthwiener  5137  harndom  8680  alephprc  9177  unialeph  9179  ndvdsi  15431  bitsfzo  15452  nprmi  15696  dec2dvds  16060  dec5dvds2  16062  mreexmrid  16583  sinhalfpilem  24521  ppi2i  25200  axlowdimlem13  26139  ex-mod  27786  measvuni  30745  ballotlem2  31019  sgnmulsgp  31081  bnj1224  31341  bnj1541  31395  bnj1311  31561  dfon2lem7  32158  onsucsuccmpi  32902  bj-imn3ani  33029  bj-0nelmpt  33518  bj-pinftynminfty  33569  poimirlem30  33884  clsk1indlem4  39040  alimp-no-surprise  43223
  Copyright terms: Public domain W3C validator