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

Theorem mtbi 310
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 216 . 2 (𝜓𝜑)
41, 3mto 186 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  mtbir  311  vprc  4719  vnex  4721  opthwiener  4892  harndom  8329  alephprc  8782  unialeph  8784  ndvdsi  14920  bitsfzo  14941  nprmi  15186  dec2dvds  15551  dec5dvds2  15553  mreexmrid  16072  sinhalfpilem  23936  ppi2i  24612  axlowdimlem13  25552  ex-mod  26464  measvuni  29410  ballotlem2  29683  sgnmulsgp  29745  bnj1224  29932  bnj1541  29986  bnj1311  30152  dfon2lem7  30744  onsucsuccmpi  31418  bj-imn3ani  31551  bj-0nelmpt  32046  bj-pinftynminfty  32087  poimirlem30  32405  clsk1indlem4  37158  alimp-no-surprise  42292
  Copyright terms: Public domain W3C validator