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

Theorem mtbi 291
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 199 . 2  |-  ( ps 
->  ph )
41, 3mto 170 1  |-  -.  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178
This theorem is referenced by:  mtbir  292  mtp-xorOLD  1547  vprc  4344  vnex  4346  opthwiener  4461  harndom  7535  alephprc  7985  unialeph  7987  ndvdsi  12935  bitsfzo  12952  nprmi  13099  dec2dvds  13404  dec5dvds2  13406  mreexmrid  13873  sinhalfpilem  20379  ppi2i  20957  measvuni  24573  ballotlem2  24751  dfon2lem7  25421  sltval2  25616  axlowdimlem13  25898  onsucsuccmpi  26198  jm2.23  27081  bnj1224  29247  bnj1541  29301  bnj1311  29467
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 179
  Copyright terms: Public domain W3C validator