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

Theorem mtbi 298
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 206 . 2  |-  ( ps 
->  ph )
41, 3mto 176 1  |-  -.  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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 185
This theorem is referenced by:  mtbir  299  vprc  4533  vnex  4535  opthwiener  4696  harndom  7885  alephprc  8375  unialeph  8377  ndvdsi  13727  bitsfzo  13744  nprmi  13891  dec2dvds  14205  dec5dvds2  14207  mreexmrid  14695  sinhalfpilem  22053  ppi2i  22635  axlowdimlem13  23347  measvuni  26768  ballotlem2  27010  sgnmulsgp  27072  dfon2lem7  27741  sltval2  27936  onsucsuccmpi  28428  alimp-no-surprise  31446  bnj1224  32108  bnj1541  32162  bnj1311  32328  bj-imn3ani  32426  bj-pinftynminfty  32869
  Copyright terms: Public domain W3C validator