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  771  ordir  817  andir  819  3anrot  983  3orrot  984  3ancoma  985  3orcomb  987  3ioran  993  3anbi123i  1188  3orbi123i  1189  3or6  1323  xorcom  1388  nfbii  1473  19.26-3an  1483  alnex  1499  19.42h  1687  19.42  1688  equsal  1727  equsalv  1793  sb6  1886  eeeanv  1933  sbbi  1959  sbco3xzyz  1973  sbcom2v  1985  sbel2x  1998  sb8eu  2039  sb8mo  2040  sb8euh  2049  eu1  2051  cbvmo  2066  mo3h  2079  sbmo  2085  eqcom  2179  abeq1  2287  cbvabw  2300  cbvab  2301  clelab  2303  nfceqi  2315  sbabel  2346  ralbii2  2487  rexbii2  2488  r2alf  2494  r2exf  2495  nfraldya  2512  nfrexdya  2513  r3al  2521  r19.41  2632  r19.42v  2634  ralcomf  2638  rexcomf  2639  reean  2645  3reeanv  2647  rabid2  2653  rabbi  2654  reubiia  2661  rmobiia  2666  reu5  2689  rmo5  2692  cbvralfw  2694  cbvrexfw  2695  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrmo  2702  cbvralvw  2707  cbvrexvw  2708  vjust  2738  ceqsex3v  2779  ceqsex4v  2780  ceqsex8v  2782  eueq  2908  reu2  2925  reu6  2926  reu3  2927  rmo4  2930  rmo3f  2934  2rmorex  2943  cbvsbcw  2990  cbvsbc  2991  sbccomlem  3037  rmo3  3054  csbcow  3068  csbabg  3118  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  eqss  3170  uniiunlem  3244  ssequn1  3305  unss  3309  rexun  3315  ralunb  3316  elin3  3326  incom  3327  inass  3345  ssin  3357  ssddif  3369  unssdif  3370  difin  3372  invdif  3377  indif  3378  indi  3382  symdifxor  3401  disj3  3475  eldifpr  3619  rexsns  3631  reusn  3663  prss  3748  tpss  3758  eluni2  3813  elunirab  3822  uniun  3828  uni0b  3834  unissb  3839  elintrab  3856  ssintrab  3867  intun  3875  intpr  3876  iuncom  3892  iuncom4  3893  iunab  3933  ssiinf  3936  iinab  3948  iunin2  3950  iunun  3965  iunxun  3966  iunxiun  3968  sspwuni  3971  iinpw  3977  cbvdisj  3990  brun  4054  brin  4055  brdif  4056  dftr2  4103  inuni  4155  repizf2lem  4161  unidif0  4167  ssext  4221  pweqb  4223  otth2  4241  opelopabsbALT  4259  eqopab2b  4279  pwin  4282  unisuc  4413  elpwpwel  4475  sucexb  4496  elomssom  4604  xpiundi  4684  xpiundir  4685  poinxp  4695  soinxp  4696  seinxp  4697  inopab  4759  difopab  4760  raliunxp  4768  rexiunxp  4769  iunxpf  4775  cnvco  4812  dmiun  4836  dmuni  4837  dm0rn0  4844  brres  4913  dmres  4928  restidsing  4963  cnvsym  5012  asymref  5014  codir  5017  qfto  5018  cnvopab  5030  cnvdif  5035  rniun  5039  dminss  5043  imainss  5044  cnvcnvsn  5105  resco  5133  imaco  5134  rnco  5135  coiun  5138  coass  5147  ressn  5169  cnviinm  5170  xpcom  5175  funcnv  5277  funcnv3  5278  fncnv  5282  fun11  5283  fnres  5332  dfmpt3  5338  fnopabg  5339  fintm  5401  fin  5402  fores  5447  dff1o3  5467  fun11iun  5482  f11o  5494  f1ompt  5667  fsn  5688  imaiun  5760  isores2  5813  eqoprab2b  5932  opabex3d  6121  opabex3  6122  dfopab2  6189  dfoprab3s  6190  fmpox  6200  tpostpos  6264  dfsmo2  6287  qsid  6599  mapval2  6677  mapsncnv  6694  elixp2  6701  ixpin  6722  xpassen  6829  diffitest  6886  pw1dc0el  6910  supmoti  6991  eqinfti  7018  distrnqg  7385  ltbtwnnq  7414  distrnq0  7457  nqprrnd  7541  ltresr  7837  elznn0nn  9266  xrnemnf  9776  xrnepnf  9777  elioomnf  9967  elxrge0  9977  elfzuzb  10018  fzass4  10061  elfz2nn0  10111  elfzo2  10149  elfzo3  10162  lbfzo0  10180  fzind2  10238  dfrp2  10263  rexfiuz  10997  fisumcom2  11445  prodmodc  11585  fprodcom2fi  11633  infssuzex  11949  infpn2  12456  xpsfrnel  12762  xpscf  12765  islmod  13379  isbasis2g  13515  tgval2  13521  ntreq0  13602  txuni2  13726  isms2  13924  bdceq  14564