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  393  pm5.32ri  459  mpan10  478  an31  570  an4  592  or4  783  ordir  829  andir  831  3anrot  1014  3orrot  1015  3ancoma  1016  3orcomb  1018  3ioran  1024  3anbi123i  1219  3orbi123i  1220  3or6  1364  xorcom  1437  nfbii  1526  19.26-3an  1536  alnex  1552  19.42h  1739  19.42  1740  equsal  1779  equsalv  1846  sb6  1941  eeeanv  1993  sbbi  2019  sbco3xzyz  2033  sbcom2v  2045  sbel2x  2058  sb8eu  2099  sb8mo  2100  sb8euh  2109  eu1  2111  cbvmo  2126  mo3h  2140  sbmo  2146  eqcom  2240  abeq1  2348  cbvabw  2363  cbvab  2364  clelab  2366  eqabcbw  2376  eqabcb  2377  nfceqi  2388  sbabel  2419  ralbii2  2560  rexbii2  2561  r2alf  2567  r2exf  2568  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.41  2706  r19.42v  2708  ralcomf  2712  rexcomf  2713  reean  2720  3reeanv  2722  rabid2  2729  rabbi  2730  cbvrmow  2735  reubiia  2738  rmobiia  2743  reu5  2770  rmo5  2773  cbvralfw  2775  cbvrexfw  2776  cbvralf  2777  cbvrexf  2778  cbvreuw  2781  cbvreu  2784  cbvrmo  2785  cbvralvw  2790  cbvrexvw  2791  vjust  2822  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  eueq  2997  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  rmo3f  3023  2rmorex  3032  cbvsbcw  3079  cbvsbc  3080  sbccomlem  3126  rmo3  3144  csbcow  3158  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  eqss  3263  uniiunlem  3338  ssequn1  3399  unss  3403  rexun  3409  ralunb  3410  elin3  3420  incom  3421  inass  3441  ssin  3453  ssddif  3465  unssdif  3466  difin  3468  invdif  3473  indif  3474  indi  3478  symdifxor  3497  ab0w  3550  disj3  3576  eldifpr  3732  rexsns  3744  reusn  3778  prss  3866  tpss  3878  eluni2  3934  elunirab  3943  uniun  3949  uni0b  3955  unissb  3960  elintrab  3977  ssintrab  3988  intun  3996  intpr  3997  iuncom  4013  iuncom4  4014  iunab  4054  ssiinf  4057  iinab  4069  iunin2  4071  iunun  4086  iunxun  4087  iunxiun  4089  sspwuni  4092  iinpw  4098  cbvdisj  4111  brun  4177  brin  4178  brdif  4179  dftr2  4226  inuni  4286  repizf2lem  4293  unidif0  4299  ssext  4356  pweqb  4358  otth2  4376  opelopabsbALT  4396  eqopab2b  4417  pwin  4422  unisuc  4553  elpwpwel  4616  sucexb  4639  elomssom  4747  xpiundi  4828  xpiundir  4829  poinxp  4839  soinxp  4840  seinxp  4841  inopab  4907  difopab  4908  raliunxp  4916  rexiunxp  4917  iunxpf  4923  cnvco  4960  dmiun  4985  dmuni  4986  dm0rn0  4993  brres  5064  dmres  5079  restidsing  5114  cnvsym  5166  asymref  5168  codir  5171  qfto  5172  cnvopab  5184  cnvdif  5189  rniun  5193  dminss  5197  imainss  5198  cnvcnvsn  5259  resco  5287  imaco  5288  rnco  5289  coiun  5292  coass  5301  ressn  5323  cnviinm  5324  xpcom  5329  funcnv  5437  funcnv3  5438  fncnv  5442  fun11  5443  fnres  5495  dfmpt3  5501  fnopabg  5502  fintm  5572  fin  5573  fores  5620  dff1o3  5640  fun11iun  5655  f11o  5668  f1ompt  5850  fsn  5871  imaiun  5956  isores2  6009  eqoprab2b  6136  opabex3d  6340  opabex3  6341  dfopab2  6413  dfoprab3s  6414  fmpox  6426  tpostpos  6525  dfsmo2  6548  qsid  6864  mapval2  6949  mapsncnv  6967  elixp2  6974  ixpin  6995  xpassen  7118  diffitest  7181  pw1dc0el  7208  supmoti  7323  eqinfti  7350  distrnqg  7744  ltbtwnnq  7773  distrnq0  7816  nqprrnd  7900  ltresr  8196  elznn0nn  9637  xrnemnf  10158  xrnepnf  10159  elioomnf  10349  elxrge0  10359  elfzuzb  10401  fzass4  10446  elfz2nn0  10497  elfzo2  10535  elfzo3  10549  lbfzo0  10570  fzind2  10636  infssuzex  10644  dfrp2  10676  rexfiuz  11733  fisumcom2  12183  prodmodc  12323  fprodcom2fi  12371  4sqlem12  13159  ballotfilemelo  13200  ballotfilem2  13206  infpn2  13325  xpsfrnel  13642  xpscf  13645  drngprop  14590  opprdrng  14593  islmod  14600  isbasis2g  15069  tgval2  15075  ntreq0  15156  txuni2  15280  isms2  15478  plyun0  15760  bdceq  16782