Theorem 3bitr4i 212

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 187	. 2 |- ( ph <-> th )
5	1, 4	bitri 184	1 |- ( ch <-> th )

Syntax hints:   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bibi2d  232  pm4.71  389  pm5.32ri  455  mpan10  474  an31  564  an4  586  or4  772  ordir  818  andir  820  3anrot  985  3orrot  986  3ancoma  987  3orcomb  989  3ioran  995  3anbi123i  1190  3orbi123i  1191  3or6  1334  xorcom  1399  nfbii  1484  19.26-3an  1494  alnex  1510  19.42h  1698  19.42  1699  equsal  1738  equsalv  1804  sb6  1898  eeeanv  1949  sbbi  1975  sbco3xzyz  1989  sbcom2v  2001  sbel2x  2014  sb8eu  2055  sb8mo  2056  sb8euh  2065  eu1  2067  cbvmo  2082  mo3h  2095  sbmo  2101  eqcom  2195  abeq1  2303  cbvabw  2316  cbvab  2317  clelab  2319  nfceqi  2332  sbabel  2363  ralbii2  2504  rexbii2  2505  r2alf  2511  r2exf  2512  nfraldya  2529  nfrexdya  2530  r3al  2538  r19.41  2649  r19.42v  2651  ralcomf  2655  rexcomf  2656  reean  2663  3reeanv  2665  rabid2  2671  rabbi  2672  reubiia  2679  rmobiia  2684  reu5  2711  rmo5  2714  cbvralfw  2716  cbvrexfw  2717  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvrmo  2725  cbvralvw  2730  cbvrexvw  2731  vjust  2761  ceqsex3v  2802  ceqsex4v  2803  ceqsex8v  2805  eueq  2931  reu2  2948  reu6  2949  reu3  2950  rmo4  2953  rmo3f  2957  2rmorex  2966  cbvsbcw  3013  cbvsbc  3014  sbccomlem  3060  rmo3  3077  csbcow  3091  csbabg  3142  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  eqss  3194  uniiunlem  3268  ssequn1  3329  unss  3333  rexun  3339  ralunb  3340  elin3  3350  incom  3351  inass  3369  ssin  3381  ssddif  3393  unssdif  3394  difin  3396  invdif  3401  indif  3402  indi  3406  symdifxor  3425  disj3  3499  eldifpr  3645  rexsns  3657  reusn  3689  prss  3774  tpss  3784  eluni2  3839  elunirab  3848  uniun  3854  uni0b  3860  unissb  3865  elintrab  3882  ssintrab  3893  intun  3901  intpr  3902  iuncom  3918  iuncom4  3919  iunab  3959  ssiinf  3962  iinab  3974  iunin2  3976  iunun  3991  iunxun  3992  iunxiun  3994  sspwuni  3997  iinpw  4003  cbvdisj  4016  brun  4080  brin  4081  brdif  4082  dftr2  4129  inuni  4184  repizf2lem  4190  unidif0  4196  ssext  4250  pweqb  4252  otth2  4270  opelopabsbALT  4289  eqopab2b  4310  pwin  4313  unisuc  4444  elpwpwel  4506  sucexb  4529  elomssom  4637  xpiundi  4717  xpiundir  4718  poinxp  4728  soinxp  4729  seinxp  4730  inopab  4794  difopab  4795  raliunxp  4803  rexiunxp  4804  iunxpf  4810  cnvco  4847  dmiun  4871  dmuni  4872  dm0rn0  4879  brres  4948  dmres  4963  restidsing  4998  cnvsym  5049  asymref  5051  codir  5054  qfto  5055  cnvopab  5067  cnvdif  5072  rniun  5076  dminss  5080  imainss  5081  cnvcnvsn  5142  resco  5170  imaco  5171  rnco  5172  coiun  5175  coass  5184  ressn  5206  cnviinm  5207  xpcom  5212  funcnv  5315  funcnv3  5316  fncnv  5320  fun11  5321  fnres  5370  dfmpt3  5376  fnopabg  5377  fintm  5439  fin  5440  fores  5486  dff1o3  5506  fun11iun  5521  f11o  5533  f1ompt  5709  fsn  5730  imaiun  5803  isores2  5856  eqoprab2b  5976  opabex3d  6173  opabex3  6174  dfopab2  6242  dfoprab3s  6243  fmpox  6253  tpostpos  6317  dfsmo2  6340  qsid  6654  mapval2  6732  mapsncnv  6749  elixp2  6756  ixpin  6777  xpassen  6884  diffitest  6943  pw1dc0el  6967  supmoti  7052  eqinfti  7079  distrnqg  7447  ltbtwnnq  7476  distrnq0  7519  nqprrnd  7603  ltresr  7899  elznn0nn  9331  xrnemnf  9843  xrnepnf  9844  elioomnf  10034  elxrge0  10044  elfzuzb  10085  fzass4  10128  elfz2nn0  10178  elfzo2  10216  elfzo3  10230  lbfzo0  10248  fzind2  10306  dfrp2  10332  rexfiuz  11133  fisumcom2  11581  prodmodc  11721  fprodcom2fi  11769  infssuzex  12086  4sqlem12  12540  infpn2  12613  xpsfrnel  12927  xpscf  12930  islmod  13787  isbasis2g  14213  tgval2  14219  ntreq0  14300  txuni2  14424  isms2  14622  plyun0  14882  bdceq  15334