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

Theorem mtbi 290
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 198 . 2  |-  ( ps 
->  ph )
41, 3mto 169 1  |-  -.  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  mtbir  291  mtp-xorOLD  1543  vprc  4301  vnex  4303  opthwiener  4418  harndom  7488  alephprc  7936  unialeph  7938  ndvdsi  12885  bitsfzo  12902  nprmi  13049  dec2dvds  13354  dec5dvds2  13356  mreexmrid  13823  sinhalfpilem  20327  ppi2i  20905  measvuni  24521  ballotlem2  24699  dfon2lem7  25359  sltval2  25524  axlowdimlem13  25797  onsucsuccmpi  26097  jm2.23  26957  bnj1224  28879  bnj1541  28933  bnj1311  29099
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 178
  Copyright terms: Public domain W3C validator