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

Theorem mtbi 299
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  |-  -.  ph
mtbi.2  |-  ( ph  <->  ps )
Assertion
Ref Expression
mtbi  |-  -.  ps

Proof of Theorem mtbi
StepHypRef Expression
1 mtbi.1 . 2  |-  -.  ph
2 mtbi.2 . . 3  |-  ( ph  <->  ps )
32biimpri 209 . 2  |-  ( ps 
->  ph )
41, 3mto 179 1  |-  -.  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
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 188
This theorem is referenced by:  mtbir  300  vprc  4505  vnex  4507  opthwiener  4665  harndom  8032  alephprc  8481  unialeph  8483  ndvdsi  14334  bitsfzo  14352  nprmi  14582  dec2dvds  14978  dec5dvds2  14980  mreexmrid  15492  sinhalfpilem  23360  ppi2i  24038  axlowdimlem13  24926  measvuni  28988  ballotlem2  29273  sgnmulsgp  29373  bnj1224  29565  bnj1541  29619  bnj1311  29785  dfon2lem7  30386  onsucsuccmpi  31052  bj-imn3ani  31119  bj-pinftynminfty  31576  poimirlem30  31877  alimp-no-surprise  40123
  Copyright terms: Public domain W3C validator