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  3099  csbcomg  3104  ordsucuniel  4615  ordsucun  4616  eloprabga  5934  oeoa  6595  ereldm  6703  boxcutc  6859  mapen  7025  mapfien  7399  wemapwe  7400  sdom2en01  7928  prlem936  8671  subcan  9102  conjmul  9477  ltrec  9637  rebtwnz  10315  xposdif  10582  infmxrgelb  10653  fseq1m1p1  10858  fllt  10938  hashfacen  11392  hashf1  11395  lenegsq  11804  dvdsmod  12585  bitsmod  12627  smueqlem  12681  rpexp  12799  eulerthlem2  12850  odzdvds  12860  pcelnn  12922  xpsle  13483  isepi  13643  fthmon  13801  pospropd  14238  mndpropd  14398  grpidpropd  14399  mhmpropd  14421  grppropd  14500  ghmnsgima  14706  mndodcong  14857  odf1  14875  odf1o1  14883  sylow3lem6  14943  lsmcntzr  14989  efgredlema  15049  cmnpropd  15098  dprdf11  15258  rngpropd  15372  dvdsrpropd  15478  abvpropd  15607  lmodprop2d  15687  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  lvecvscan  15864  lvecvscan2  15865  assapropd  16067  chrnzr  16484  zndvds0  16504  ip2eq  16557  phlpropd  16559  qtopcn  17405  tsmsf1o  17827  xmetgt0  17922  txmetcnp  18093  nlmmul0or  18194  cnmet  18281  evth  18457  minveclem3b  18792  mbfposr  19007  itg2cn  19118  iblcnlem  19143  dvcvx  19367  ulm2  19764  efeq1  19891  dcubic  20142  mcubic  20143  dquart  20149  birthdaylem3  20248  ftalem2  20311  issqf  20374  sqff1o  20420  bposlem7  20529  lgsabs1  20573  lgsquadlem2  20594  dchrisum0lem1  20665  nmounbi  21354  ip2eqi  21435  hvmulcan  21651  hvsubcan2  21654  hi2eq  21684  fh2  22198  riesz4i  22643  cvbr4i  22947  ballotlemfc0  23051  ballotlemfcc  23052  xdivpnfrp  23117  subfacp1lem5  23715  eupath2lem3  23903  divelunit  24080  mulcan1g  24084  dvreasin  24923  elo  25041  1ded  25738  topfneec2  26292  neibastop3  26311  caures  26476  ismtyima  26527  isdmn3  26699  rusbcALT  27639  infrglb  27722  climreeq  27739  cusgra2v  28158  sbc3org  28295  tendospcanN  31213  dochsncom  31572
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