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  4948  vnex  4950  opthwiener  5124  harndom  8636  alephprc  9132  unialeph  9134  ndvdsi  15358  bitsfzo  15379  nprmi  15624  dec2dvds  15989  dec5dvds2  15991  mreexmrid  16525  sinhalfpilem  24435  ppi2i  25115  axlowdimlem13  26054  ex-mod  27638  measvuni  30607  ballotlem2  30880  sgnmulsgp  30942  bnj1224  31200  bnj1541  31254  bnj1311  31420  dfon2lem7  32020  onsucsuccmpi  32769  bj-imn3ani  32900  bj-0nelmpt  33393  bj-pinftynminfty  33443  poimirlem30  33770  clsk1indlem4  38862  alimp-no-surprise  43058
  Copyright terms: Public domain W3C validator