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  vnex  5259  opthwiener  5462  epelg  5525  harndom  9467  alephprc  10009  unialeph  10011  ndvdsi  16339  nprmi  16616  dec2dvds  16991  dec5dvds2  16993  mreexmrid  17566  sinhalfpilem  26428  ppi2i  27135  axlowdimlem13  29027  ex-mod  30524  sgnmulsgp  32924  measvuni  34371  ballotlem2  34646  bnj1224  34957  bnj1541  35012  bnj1311  35180  dfon2lem7  35981  onsucsuccmpi  36637  bj-imn3ani  36787  sbn1ALT  37059  bj-0nelmpt  37321  bj-pinftynminfty  37432  poimirlem30  37851  clsk1indlem4  44285  tannpoly  47136  alimp-no-surprise  50026
  Copyright terms: Public domain W3C validator