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  4285  vnex  5258  opthwiener  5458  epelg  5525  harndom  9419  alephprc  9956  unialeph  9958  ndvdsi  16220  nprmi  16491  dec2dvds  16861  dec5dvds2  16863  mreexmrid  17449  sinhalfpilem  25726  ppi2i  26424  axlowdimlem13  27611  ex-mod  29101  measvuni  32480  ballotlem2  32755  sgnmulsgp  32817  bnj1224  33080  bnj1541  33135  bnj1311  33303  dfon2lem7  34048  onsucsuccmpi  34728  bj-imn3ani  34865  sbn1ALT  35137  bj-0nelmpt  35392  bj-pinftynminfty  35503  poimirlem30  35912  clsk1indlem4  41975  alimp-no-surprise  46836
  Copyright terms: Public domain W3C validator