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

Theorem 3bitr3d 274
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
Hypotheses
Ref Expression
3bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
3bitr3d.3  |-  ( ph  ->  ( ch  <->  ta )
)
Assertion
Ref Expression
3bitr3d  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3  |-  ( ph  ->  ( ps  <->  th )
)
2 3bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr3d 246 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
53, 4bitrd 244 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbcne12g  3112  csbcomg  3117  ordsucuniel  4631  ordsucun  4632  eloprabga  5950  oeoa  6611  ereldm  6719  boxcutc  6875  mapen  7041  mapfien  7415  wemapwe  7416  sdom2en01  7944  prlem936  8687  subcan  9118  conjmul  9493  ltrec  9653  rebtwnz  10331  xposdif  10598  infmxrgelb  10669  fseq1m1p1  10874  fllt  10954  hashfacen  11408  hashf1  11411  lenegsq  11820  dvdsmod  12601  bitsmod  12643  smueqlem  12697  rpexp  12815  eulerthlem2  12866  odzdvds  12876  pcelnn  12938  xpsle  13499  isepi  13659  fthmon  13817  pospropd  14254  mndpropd  14414  grpidpropd  14415  mhmpropd  14437  grppropd  14516  ghmnsgima  14722  mndodcong  14873  odf1  14891  odf1o1  14899  sylow3lem6  14959  lsmcntzr  15005  efgredlema  15065  cmnpropd  15114  dprdf11  15274  rngpropd  15388  dvdsrpropd  15494  abvpropd  15623  lmodprop2d  15703  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  lvecvscan  15880  lvecvscan2  15881  assapropd  16083  chrnzr  16500  zndvds0  16520  ip2eq  16573  phlpropd  16575  qtopcn  17421  tsmsf1o  17843  xmetgt0  17938  txmetcnp  18109  nlmmul0or  18210  cnmet  18297  evth  18473  minveclem3b  18808  mbfposr  19023  itg2cn  19134  iblcnlem  19159  dvcvx  19383  ulm2  19780  efeq1  19907  dcubic  20158  mcubic  20159  dquart  20165  birthdaylem3  20264  ftalem2  20327  issqf  20390  sqff1o  20436  bposlem7  20545  lgsabs1  20589  lgsquadlem2  20610  dchrisum0lem1  20681  nmounbi  21370  ip2eqi  21451  hvmulcan  21667  hvsubcan2  21670  hi2eq  21700  fh2  22214  riesz4i  22659  cvbr4i  22963  ballotlemfc0  23067  ballotlemfcc  23068  xdivpnfrp  23133  subfacp1lem5  23730  eupath2lem3  23918  divelunit  24095  mulcan1g  24099  itgaddnclem2  25010  dvreasin  25026  elo  25144  1ded  25841  topfneec2  26395  neibastop3  26414  caures  26579  ismtyima  26630  isdmn3  26802  rusbcALT  27742  infrglb  27825  climreeq  27842  cusgra2v  28297  sbc3org  28594  tendospcanN  31835  dochsncom  32194
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