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  776  ordir  822  andir  824  3anrot  1007  3orrot  1008  3ancoma  1009  3orcomb  1011  3ioran  1017  3anbi123i  1212  3orbi123i  1213  3or6  1357  xorcom  1430  nfbii  1519  19.26-3an  1529  alnex  1545  19.42h  1733  19.42  1734  equsal  1773  equsalv  1839  sb6  1933  eeeanv  1984  sbbi  2010  sbco3xzyz  2024  sbcom2v  2036  sbel2x  2049  sb8eu  2090  sb8mo  2091  sb8euh  2100  eu1  2102  cbvmo  2117  mo3h  2131  sbmo  2137  eqcom  2231  abeq1  2339  cbvabw  2352  cbvab  2353  clelab  2355  nfceqi  2368  sbabel  2399  ralbii2  2540  rexbii2  2541  r2alf  2547  r2exf  2548  nfraldya  2565  nfrexdya  2566  r3al  2574  r19.41  2686  r19.42v  2688  ralcomf  2692  rexcomf  2693  reean  2700  3reeanv  2702  rabid2  2708  rabbi  2709  cbvrmow  2714  reubiia  2717  rmobiia  2722  reu5  2749  rmo5  2752  cbvralfw  2754  cbvrexfw  2755  cbvralf  2756  cbvrexf  2757  cbvreuw  2760  cbvreu  2763  cbvrmo  2764  cbvralvw  2769  cbvrexvw  2770  vjust  2800  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  eueq  2974  reu2  2991  reu6  2992  reu3  2993  rmo4  2996  rmo3f  3000  2rmorex  3009  cbvsbcw  3056  cbvsbc  3057  sbccomlem  3103  rmo3  3121  csbcow  3135  csbabg  3186  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  eqss  3239  uniiunlem  3313  ssequn1  3374  unss  3378  rexun  3384  ralunb  3385  elin3  3395  incom  3396  inass  3414  ssin  3426  ssddif  3438  unssdif  3439  difin  3441  invdif  3446  indif  3447  indi  3451  symdifxor  3470  disj3  3544  eldifpr  3693  rexsns  3705  reusn  3737  prss  3824  tpss  3836  eluni2  3892  elunirab  3901  uniun  3907  uni0b  3913  unissb  3918  elintrab  3935  ssintrab  3946  intun  3954  intpr  3955  iuncom  3971  iuncom4  3972  iunab  4012  ssiinf  4015  iinab  4027  iunin2  4029  iunun  4044  iunxun  4045  iunxiun  4047  sspwuni  4050  iinpw  4056  cbvdisj  4069  brun  4135  brin  4136  brdif  4137  dftr2  4184  inuni  4239  repizf2lem  4245  unidif0  4251  ssext  4307  pweqb  4309  otth2  4327  opelopabsbALT  4347  eqopab2b  4368  pwin  4373  unisuc  4504  elpwpwel  4566  sucexb  4589  elomssom  4697  xpiundi  4777  xpiundir  4778  poinxp  4788  soinxp  4789  seinxp  4790  inopab  4854  difopab  4855  raliunxp  4863  rexiunxp  4864  iunxpf  4870  cnvco  4907  dmiun  4932  dmuni  4933  dm0rn0  4940  brres  5011  dmres  5026  restidsing  5061  cnvsym  5112  asymref  5114  codir  5117  qfto  5118  cnvopab  5130  cnvdif  5135  rniun  5139  dminss  5143  imainss  5144  cnvcnvsn  5205  resco  5233  imaco  5234  rnco  5235  coiun  5238  coass  5247  ressn  5269  cnviinm  5270  xpcom  5275  funcnv  5382  funcnv3  5383  fncnv  5387  fun11  5388  fnres  5440  dfmpt3  5446  fnopabg  5447  fintm  5511  fin  5512  fores  5558  dff1o3  5578  fun11iun  5593  f11o  5605  f1ompt  5786  fsn  5807  imaiun  5884  isores2  5937  eqoprab2b  6062  opabex3d  6266  opabex3  6267  dfopab2  6335  dfoprab3s  6336  fmpox  6346  tpostpos  6410  dfsmo2  6433  qsid  6747  mapval2  6825  mapsncnv  6842  elixp2  6849  ixpin  6870  xpassen  6989  diffitest  7049  pw1dc0el  7073  supmoti  7160  eqinfti  7187  distrnqg  7574  ltbtwnnq  7603  distrnq0  7646  nqprrnd  7730  ltresr  8026  elznn0nn  9460  xrnemnf  9973  xrnepnf  9974  elioomnf  10164  elxrge0  10174  elfzuzb  10215  fzass4  10258  elfz2nn0  10308  elfzo2  10346  elfzo3  10360  lbfzo0  10381  fzind2  10445  infssuzex  10453  dfrp2  10483  rexfiuz  11500  fisumcom2  11949  prodmodc  12089  fprodcom2fi  12137  4sqlem12  12925  infpn2  13027  xpsfrnel  13377  xpscf  13380  islmod  14255  isbasis2g  14719  tgval2  14725  ntreq0  14806  txuni2  14930  isms2  15128  plyun0  15410  bdceq  16205