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

Theorem mtbi 321
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 227 . 2 (𝜓𝜑)
41, 3mto 196 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  mtbir  322  vn0  4341  vnex  5319  opthwiener  5520  epelg  5587  harndom  9605  alephprc  10142  unialeph  10144  ndvdsi  16414  nprmi  16690  dec2dvds  17065  dec5dvds2  17067  mreexmrid  17656  sinhalfpilem  26491  ppi2i  27197  axlowdimlem13  28888  ex-mod  30382  measvuni  34047  ballotlem2  34322  sgnmulsgp  34384  bnj1224  34646  bnj1541  34701  bnj1311  34869  dfon2lem7  35613  onsucsuccmpi  36155  bj-imn3ani  36292  sbn1ALT  36563  bj-0nelmpt  36823  bj-pinftynminfty  36934  poimirlem30  37351  clsk1indlem4  43711  alimp-no-surprise  48529
  Copyright terms: Public domain W3C validator