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

Theorem mtbi 323
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 229 . 2 (𝜓𝜑)
41, 3mto 198 1 ¬ 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  mtbir  324  vnex  5209  opthwiener  5395  epelg  5459  harndom  9016  alephprc  9513  unialeph  9515  ndvdsi  15751  nprmi  16021  dec2dvds  16387  dec5dvds2  16389  mreexmrid  16902  sinhalfpilem  24976  ppi2i  25673  axlowdimlem13  26667  ex-mod  28155  measvuni  31372  ballotlem2  31645  sgnmulsgp  31707  bnj1224  31972  bnj1541  32027  bnj1311  32193  dfon2lem7  32931  onsucsuccmpi  33688  bj-imn3ani  33818  bj-0nelmpt  34300  bj-pinftynminfty  34401  poimirlem30  34803  clsk1indlem4  40272  alimp-no-surprise  44810
  Copyright terms: Public domain W3C validator