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-xor  1525  vprc  4152  vnex  4154  opthwiener  4268  harndom  7278  alephprc  7726  unialeph  7728  ndvdsi  12609  bitsfzo  12626  nprmi  12773  dec2dvds  13078  dec5dvds2  13080  mreexmrid  13545  sinhalfpilem  19834  ppi2i  20407  measvuni  23542  dfon2lem7  24145  sltval2  24310  axlowdimlem13  24582  onsucsuccmpi  24882  jm2.23  27089  compneOLD  27643  bnj1224  28834  bnj1541  28888  bnj1311  29054
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