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  5112  opthwiener  5298  epelg  5357  harndom  8877  alephprc  9374  unialeph  9376  ndvdsi  15596  nprmi  15862  dec2dvds  16228  dec5dvds2  16230  mreexmrid  16743  sinhalfpilem  24732  ppi2i  25428  axlowdimlem13  26423  ex-mod  27912  measvuni  31082  ballotlem2  31355  sgnmulsgp  31417  bnj1224  31682  bnj1541  31736  bnj1311  31902  dfon2lem7  32636  onsucsuccmpi  33394  bj-imn3ani  33524  bj-0nelmpt  34019  bj-pinftynminfty  34080  poimirlem30  34466  clsk1indlem4  39892  alimp-no-surprise  44376
  Copyright terms: Public domain W3C validator