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

Theorem mtbi 322
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 228 . 2 (𝜓𝜑)
41, 3mto 197 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206
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 207
This theorem is referenced by:  mtbir  323  vn0  4344  vnex  5313  opthwiener  5518  epelg  5584  harndom  9603  alephprc  10140  unialeph  10142  ndvdsi  16450  nprmi  16727  dec2dvds  17102  dec5dvds2  17104  mreexmrid  17687  sinhalfpilem  26506  ppi2i  27213  axlowdimlem13  28970  ex-mod  30469  measvuni  34216  ballotlem2  34492  sgnmulsgp  34554  bnj1224  34816  bnj1541  34871  bnj1311  35039  dfon2lem7  35791  onsucsuccmpi  36445  bj-imn3ani  36589  sbn1ALT  36860  bj-0nelmpt  37118  bj-pinftynminfty  37229  poimirlem30  37658  clsk1indlem4  44062  alimp-no-surprise  49355
  Copyright terms: Public domain W3C validator