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  3674  sbcne12gOLD  3675  csbcomgOLD  3685  fnprb  5931  eloprabga  6172  ordsucuniel  6430  ordsucun  6431  oeoa  7028  ereldm  7136  boxcutc  7298  mapen  7467  mapfien  7649  mapfienOLD  7919  wemapwe  7920  wemapweOLD  7921  sdom2en01  8463  prlem936  9208  subcan  9656  mulcan1g  9981  conjmul  10040  ltrec  10205  rebtwnz  10944  xposdif  11217  infmxrgelb  11289  divelunit  11419  fseq1m1p1  11527  fllt  11648  hashfacen  12199  hashf1  12202  lenegsq  12800  dvdsmod  13582  bitsmod  13624  smueqlem  13678  rpexp  13798  eulerthlem2  13849  odzdvds  13859  pcelnn  13928  xpsle  14511  isepi  14671  fthmon  14829  pospropd  15296  mndpropd  15438  grpidpropd  15439  mhmpropd  15462  grppropd  15547  ghmnsgima  15761  mndodcong  16036  odf1  16054  odf1o1  16062  sylow3lem6  16122  lsmcntzr  16168  efgredlema  16228  cmnpropd  16277  dprdf11  16501  dprdf11OLD  16508  rngpropd  16664  dvdsrpropd  16776  abvpropd  16905  lmodprop2d  16985  lsspropd  17075  lmhmpropd  17131  lbspropd  17157  lvecvscan  17169  lvecvscan2  17170  assapropd  17375  chrnzr  17936  zndvds0  17958  ip2eq  18057  phlpropd  18059  qtopcn  19262  tsmsf1o  19694  xmetgt0  19908  txmetcnp  20097  metustsymOLD  20111  metustsym  20112  nlmmul0or  20239  cnmet  20326  evth  20506  minveclem3b  20890  mbfposr  21105  itg2cn  21216  iblcnlem  21241  dvcvx  21467  ulm2  21825  efeq1  21960  dcubic  22216  mcubic  22217  dquart  22223  birthdaylem3  22322  ftalem2  22386  issqf  22449  sqff1o  22495  bposlem7  22604  lgsabs1  22648  lgsquadlem2  22669  dchrisum0lem1  22740  cusgra2v  23321  eupath2lem3  23551  nmounbi  24127  ip2eqi  24208  hvmulcan  24425  hvsubcan2  24428  hi2eq  24458  fh2  24973  riesz4i  25418  cvbr4i  25722  xdivpnfrp  26059  isorng  26218  ballotlemfc0  26827  ballotlemfcc  26828  sgnmulsgn  26884  sgnmulsgp  26885  subfacp1lem5  27024  cos2h  28376  tan2h  28377  dvasin  28433  topfneec2  28517  neibastop3  28536  caures  28609  ismtyima  28655  isdmn3  28827  rusbcALT  29646  infrglb  29724  climreeq  29739  sbc3orgOLD  31125  tendospcanN  34508  dochsncom  34867