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  4351  vnex  5320  opthwiener  5524  epelg  5590  harndom  9600  alephprc  10137  unialeph  10139  ndvdsi  16446  nprmi  16723  dec2dvds  17097  dec5dvds2  17099  mreexmrid  17688  sinhalfpilem  26520  ppi2i  27227  axlowdimlem13  28984  ex-mod  30478  measvuni  34195  ballotlem2  34470  sgnmulsgp  34532  bnj1224  34794  bnj1541  34849  bnj1311  35017  dfon2lem7  35771  onsucsuccmpi  36426  bj-imn3ani  36570  sbn1ALT  36841  bj-0nelmpt  37099  bj-pinftynminfty  37210  poimirlem30  37637  clsk1indlem4  44034  alimp-no-surprise  49012
  Copyright terms: Public domain W3C validator