Theorem 3bitr4i 211

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	|- ( ph <-> ps )
3bitr4i.2	|- ( ch <-> ph )
3bitr4i.3	|- ( th <-> ps )

Assertion

Ref	Expression
3bitr4i	|- ( ch <-> th )

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- ( ch <-> ph )
2		3bitr4i.1	. . 3 |- ( ph <-> ps )
3		3bitr4i.3	. . 3 |- ( th <-> ps )
4	2, 3	bitr4i 186	. 2 |- ( ph <-> th )
5	1, 4	bitri 183	1 |- ( ch <-> th )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi2d  231  pm4.71  382  pm5.32ri  444  mpan10  459  an31  532  an4  554  or4  726  ordir  769  andir  771  dcbii  788  3anrot  932  3orrot  933  3ancoma  934  3orcomb  936  3ioran  942  3anbi123i  1135  3orbi123i  1136  3or6  1266  xorcom  1331  nfbii  1414  19.26-3an  1424  alnex  1440  19.42h  1629  19.42  1630  equsal  1669  sb6  1821  eeeanv  1863  sbbi  1888  sbco3xzyz  1902  sbcom2v  1916  sbel2x  1929  sb8eu  1968  sb8mo  1969  sb8euh  1978  eu1  1980  cbvmo  1995  mo3h  2008  sbmo  2014  eqcom  2097  abeq1  2204  cbvab  2217  clelab  2219  nfceqi  2231  sbabel  2261  ralbii2  2399  rexbii2  2400  r2alf  2406  r2exf  2407  nfraldya  2423  nfrexdya  2424  r3al  2431  r19.41  2536  r19.42v  2538  ralcomf  2542  rexcomf  2543  reean  2549  3reeanv  2551  rabid2  2557  rabbi  2558  reubiia  2565  rmobiia  2570  reu5  2593  rmo5  2596  cbvralf  2598  cbvrexf  2599  cbvreu  2602  cbvrmo  2603  vjust  2634  ceqsex3v  2675  ceqsex4v  2676  ceqsex8v  2678  eueq  2800  reu2  2817  reu6  2818  reu3  2819  rmo4  2822  rmo3f  2826  2rmorex  2835  cbvsbc  2881  sbccomlem  2927  rmo3  2944  csbabg  3003  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  eqss  3054  uniiunlem  3124  ssequn1  3185  unss  3189  rexun  3195  ralunb  3196  elin3  3206  incom  3207  inass  3225  ssin  3237  ssddif  3249  unssdif  3250  difin  3252  invdif  3257  indif  3258  indi  3262  symdifxor  3281  disj3  3354  rexsns  3502  reusn  3533  prss  3615  tpss  3624  eluni2  3679  elunirab  3688  uniun  3694  uni0b  3700  unissb  3705  elintrab  3722  ssintrab  3733  intun  3741  intpr  3742  iuncom  3758  iuncom4  3759  iunab  3798  ssiinf  3801  iinab  3813  iunin2  3815  iunun  3830  iunxun  3831  iunxiun  3832  sspwuni  3835  iinpw  3841  cbvdisj  3854  brun  3913  brin  3914  brdif  3915  dftr2  3960  inuni  4012  repizf2lem  4017  unidif0  4023  ssext  4072  pweqb  4074  otth2  4092  opelopabsbALT  4110  eqopab2b  4130  pwin  4133  unisuc  4264  elpwpwel  4325  sucexb  4342  elnn  4448  xpiundi  4525  xpiundir  4526  poinxp  4536  soinxp  4537  seinxp  4538  inopab  4599  difopab  4600  raliunxp  4608  rexiunxp  4609  iunxpf  4615  cnvco  4652  dmiun  4676  dmuni  4677  dm0rn0  4684  brres  4751  dmres  4766  cnvsym  4848  asymref  4850  codir  4853  qfto  4854  cnvopab  4866  cnvdif  4871  rniun  4875  dminss  4879  imainss  4880  cnvcnvsn  4941  resco  4969  imaco  4970  rnco  4971  coiun  4974  coass  4983  ressn  5005  cnviinm  5006  xpcom  5011  funcnv  5109  funcnv3  5110  fncnv  5114  fun11  5115  fnres  5164  dfmpt3  5170  fnopabg  5171  fintm  5231  fin  5232  fores  5277  dff1o3  5294  fun11iun  5309  f11o  5321  f1ompt  5489  fsn  5508  imaiun  5577  isores2  5630  eqoprab2b  5745  opabex3d  5930  opabex3  5931  dfopab2  5997  dfoprab3s  5998  fmpt2x  6008  tpostpos  6067  dfsmo2  6090  qsid  6397  mapval2  6475  mapsncnv  6492  elixp2  6499  ixpin  6520  xpassen  6626  diffitest  6683  supmoti  6768  eqinfti  6795  distrnqg  7043  ltbtwnnq  7072  distrnq0  7115  nqprrnd  7199  ltresr  7473  elznn0nn  8862  xrnemnf  9347  xrnepnf  9348  elioomnf  9534  elxrge0  9544  elfzuzb  9583  fzass4  9625  elfz2nn0  9675  elfzo2  9710  elfzo3  9723  lbfzo0  9741  fzind2  9799  rexfiuz  10553  fisumcom2  10997  infssuzex  11388  isbasis2g  11911  tgval2  11919  ntreq0  12000  isms2  12256  bdceq  12457