Theorem 3bitr3d 287

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 259	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 257	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 188

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 189

This theorem is referenced by:  sbcne12  3804  fnprb  6136  eloprabga  6395  ordsucuniel  6663  ordsucun  6664  oeoa  7304  ereldm  7413  boxcutc  7571  mapen  7740  mapfien  7925  wemapwe  8205  sdom2en01  8734  prlem936  9474  subcan  9931  mulcan1g  10267  conjmul  10326  ltrec  10490  rebtwnz  11265  xposdif  11550  infmxrgelbOLD  11627  divelunit  11776  fseq1m1p1  11871  fzm1  11876  fllt  12043  hashfacen  12616  hashf1  12619  lenegsq  13377  dvdsmod  14355  bitsmod  14403  smueqlem  14457  rpexp  14665  eulerthlem2  14723  odzdvds  14733  odzdvdsOLD  14739  pcelnn  14812  xpsle  15480  isepi  15638  fthmon  15825  pospropd  16373  grpidpropd  16497  mndpropd  16555  mhmpropd  16581  grppropd  16677  ghmnsgima  16899  mndodcong  17184  odf1  17206  odf1o1  17214  sylow3lem6  17277  lsmcntzr  17323  efgredlema  17383  cmnpropd  17432  dprdf11  17649  ringpropd  17805  dvdsrpropd  17917  abvpropd  18063  lmodprop2d  18143  lsspropd  18233  lmhmpropd  18289  lbspropd  18315  lvecvscan  18327  lvecvscan2  18328  assapropd  18544  chrnzr  19093  zndvds0  19113  ip2eq  19212  phlpropd  19214  qtopcn  20721  tsmsf1o  21151  xmetgt0  21365  txmetcnp  21554  metustsym  21562  nlmmul0or  21678  cnmet  21784  evth  21979  minveclem3b  22362  minveclem3bOLD  22374  mbfposr  22600  itg2cn  22713  iblcnlem  22738  dvcvx  22964  ulm2  23332  efeq1  23470  dcubic  23764  mcubic  23765  dquart  23771  birthdaylem3  23871  ftalem2  23990  issqf  24055  sqff1o  24101  bposlem7  24210  lgsabs1  24254  lgsquadlem2  24275  dchrisum0lem1  24346  opphllem6  24786  colhp  24804  lmiinv  24826  lmiopp  24836  cusgra2v  25182  eupath2lem3  25699  nmounbi  26409  ip2eqi  26490  hvmulcan  26717  hvsubcan2  26720  hi2eq  26750  fh2  27264  riesz4i  27708  cvbr4i  28012  infxrge0glbOLD  28349  xdivpnfrp  28403  isorng  28564  ballotlemfc0  29327  ballotlemfcc  29328  sgnmulsgn  29422  sgnmulsgp  29423  subfacp1lem5  29909  topfneec2  31011  neibastop3  31017  cos2h  31856  tan2h  31857  poimirlem25  31885  poimirlem27  31887  dvasin  31948  caures  32009  ismtyima  32055  isdmn3  32227  tendospcanN  34516  dochsncom  34875  rusbcALT  36654  sbc3orgOLD  36757  infrglbOLD  37495  climreeq  37519  coseq0  37565  mgmhmpropd  39089