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  4594  vnex  4596  opthwiener  4758  harndom  8008  alephprc  8497  unialeph  8499  ndvdsi  14080  bitsfzo  14097  nprmi  14244  dec2dvds  14561  dec5dvds2  14563  mreexmrid  15060  sinhalfpilem  22982  ppi2i  23569  axlowdimlem13  24384  measvuni  28358  ballotlem2  28624  sgnmulsgp  28686  dfon2lem7  29438  onsucsuccmpi  30113  alimp-no-surprise  33340  bnj1224  34003  bnj1541  34057  bnj1311  34223  bj-imn3ani  34319  bj-pinftynminfty  34773
  Copyright terms: Public domain W3C validator