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

Theorem mtbi 289
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 197 . 2  |-  ( ps 
->  ph )
41, 3mto 167 1  |-  -.  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  mtbir  290  mtp-xorOLD  1542  vprc  4254  vnex  4256  opthwiener  4371  harndom  7425  alephprc  7873  unialeph  7875  ndvdsi  12817  bitsfzo  12834  nprmi  12981  dec2dvds  13286  dec5dvds2  13288  mreexmrid  13755  sinhalfpilem  20052  ppi2i  20630  measvuni  24152  dfon2lem7  24971  sltval2  25136  axlowdimlem13  25409  onsucsuccmpi  25709  jm2.23  26680  compneOLD  27234  bnj1224  28586  bnj1541  28640  bnj1311  28806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator