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  2803  ceqsex4v  2804  ceqsex8v  2806  eueq  2932  reu2  2949  reu6  2950  reu3  2951  rmo4  2954  rmo3f  2958  2rmorex  2967  cbvsbcw  3014  cbvsbc  3015  sbccomlem  3061  rmo3  3078  csbcow  3092  csbabg  3143  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  eqss  3195  uniiunlem  3269  ssequn1  3330  unss  3334  rexun  3340  ralunb  3341  elin3  3351  incom  3352  inass  3370  ssin  3382  ssddif  3394  unssdif  3395  difin  3397  invdif  3402  indif  3403  indi  3407  symdifxor  3426  disj3  3500  eldifpr  3646  rexsns  3658  reusn  3690  prss  3775  tpss  3785  eluni2  3840  elunirab  3849  uniun  3855  uni0b  3861  unissb  3866  elintrab  3883  ssintrab  3894  intun  3902  intpr  3903  iuncom  3919  iuncom4  3920  iunab  3960  ssiinf  3963  iinab  3975  iunin2  3977  iunun  3992  iunxun  3993  iunxiun  3995  sspwuni  3998  iinpw  4004  cbvdisj  4017  brun  4081  brin  4082  brdif  4083  dftr2  4130  inuni  4185  repizf2lem  4191  unidif0  4197  ssext  4251  pweqb  4253  otth2  4271  opelopabsbALT  4290  eqopab2b  4311  pwin  4314  unisuc  4445  elpwpwel  4507  sucexb  4530  elomssom  4638  xpiundi  4718  xpiundir  4719  poinxp  4729  soinxp  4730  seinxp  4731  inopab  4795  difopab  4796  raliunxp  4804  rexiunxp  4805  iunxpf  4811  cnvco  4848  dmiun  4872  dmuni  4873  dm0rn0  4880  brres  4949  dmres  4964  restidsing  4999  cnvsym  5050  asymref  5052  codir  5055  qfto  5056  cnvopab  5068  cnvdif  5073  rniun  5077  dminss  5081  imainss  5082  cnvcnvsn  5143  resco  5171  imaco  5172  rnco  5173  coiun  5176  coass  5185  ressn  5207  cnviinm  5208  xpcom  5213  funcnv  5316  funcnv3  5317  fncnv  5321  fun11  5322  fnres  5371  dfmpt3  5377  fnopabg  5378  fintm  5440  fin  5441  fores  5487  dff1o3  5507  fun11iun  5522  f11o  5534  f1ompt  5710  fsn  5731  imaiun  5804  isores2  5857  eqoprab2b  5977  opabex3d  6175  opabex3  6176  dfopab2  6244  dfoprab3s  6245  fmpox  6255  tpostpos  6319  dfsmo2  6342  qsid  6656  mapval2  6734  mapsncnv  6751  elixp2  6758  ixpin  6779  xpassen  6886  diffitest  6945  pw1dc0el  6969  supmoti  7054  eqinfti  7081  distrnqg  7449  ltbtwnnq  7478  distrnq0  7521  nqprrnd  7605  ltresr  7901  elznn0nn  9334  xrnemnf  9846  xrnepnf  9847  elioomnf  10037  elxrge0  10047  elfzuzb  10088  fzass4  10131  elfz2nn0  10181  elfzo2  10219  elfzo3  10233  lbfzo0  10251  fzind2  10309  dfrp2  10335  rexfiuz  11136  fisumcom2  11584  prodmodc  11724  fprodcom2fi  11772  infssuzex  12089  4sqlem12  12543  infpn2  12616  xpsfrnel  12930  xpscf  12933  islmod  13790  isbasis2g  14224  tgval2  14230  ntreq0  14311  txuni2  14435  isms2  14633  plyun0  14915  bdceq  15404