Theorem 3bitr3d 283

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

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 |- ( ph -> ( ps <-> th ) )
2		3bitr3d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr3d 255	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 253	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> 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:  sbcne12  3820  sbcne12gOLD  3821  csbcomgOLD  3831  fnprb  6110  eloprabga  6364  ordsucuniel  6630  ordsucun  6631  oeoa  7236  ereldm  7345  boxcutc  7502  mapen  7671  mapfien  7856  mapfienOLD  8127  wemapwe  8128  wemapweOLD  8129  sdom2en01  8671  prlem936  9414  subcan  9863  mulcan1g  10191  conjmul  10250  ltrec  10415  rebtwnz  11170  xposdif  11443  infmxrgelb  11515  divelunit  11651  fseq1m1p1  11742  fllt  11900  hashfacen  12456  hashf1  12459  lenegsq  13102  dvdsmod  13891  bitsmod  13934  smueqlem  13988  rpexp  14109  eulerthlem2  14160  odzdvds  14170  pcelnn  14241  xpsle  14825  isepi  14985  fthmon  15143  pospropd  15610  mndpropd  15752  grpidpropd  15753  mhmpropd  15776  grppropd  15862  ghmnsgima  16078  mndodcong  16355  odf1  16373  odf1o1  16381  sylow3lem6  16441  lsmcntzr  16487  efgredlema  16547  cmnpropd  16596  dprdf11  16846  dprdf11OLD  16853  rngpropd  17010  dvdsrpropd  17122  abvpropd  17267  lmodprop2d  17348  lsspropd  17439  lmhmpropd  17495  lbspropd  17521  lvecvscan  17533  lvecvscan2  17534  assapropd  17740  chrnzr  18327  zndvds0  18349  ip2eq  18448  phlpropd  18450  qtopcn  19943  tsmsf1o  20375  xmetgt0  20589  txmetcnp  20778  metustsymOLD  20792  metustsym  20793  nlmmul0or  20920  cnmet  21007  evth  21187  minveclem3b  21571  mbfposr  21787  itg2cn  21898  iblcnlem  21923  dvcvx  22149  ulm2  22507  efeq1  22642  dcubic  22898  mcubic  22899  dquart  22905  birthdaylem3  23004  ftalem2  23068  issqf  23131  sqff1o  23177  bposlem7  23286  lgsabs1  23330  lgsquadlem2  23351  dchrisum0lem1  23422  lmiinv  23828  cusgra2v  24124  eupath2lem3  24641  nmounbi  25217  ip2eqi  25298  hvmulcan  25515  hvsubcan2  25518  hi2eq  25548  fh2  26063  riesz4i  26508  cvbr4i  26812  xdivpnfrp  27147  isorng  27302  ballotlemfc0  27921  ballotlemfcc  27922  sgnmulsgn  27978  sgnmulsgp  27979  subfacp1lem5  28118  cos2h  29474  tan2h  29475  dvasin  29531  topfneec2  29615  neibastop3  29634  caures  29707  ismtyima  29753  isdmn3  29925  rusbcALT  30743  infrglb  30959  climreeq  30974  coseq0  31018  sbc3orgOLD  32257  tendospcanN  35695  dochsncom  36054