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  1487  19.26-3an  1497  alnex  1513  19.42h  1701  19.42  1702  equsal  1741  equsalv  1807  sb6  1901  eeeanv  1952  sbbi  1978  sbco3xzyz  1992  sbcom2v  2004  sbel2x  2017  sb8eu  2058  sb8mo  2059  sb8euh  2068  eu1  2070  cbvmo  2085  mo3h  2098  sbmo  2104  eqcom  2198  abeq1  2306  cbvabw  2319  cbvab  2320  clelab  2322  nfceqi  2335  sbabel  2366  ralbii2  2507  rexbii2  2508  r2alf  2514  r2exf  2515  nfraldya  2532  nfrexdya  2533  r3al  2541  r19.41  2652  r19.42v  2654  ralcomf  2658  rexcomf  2659  reean  2666  3reeanv  2668  rabid2  2674  rabbi  2675  reubiia  2682  rmobiia  2687  reu5  2714  rmo5  2717  cbvralfw  2719  cbvrexfw  2720  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrmo  2728  cbvralvw  2733  cbvrexvw  2734  vjust  2764  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  eueq  2935  reu2  2952  reu6  2953  reu3  2954  rmo4  2957  rmo3f  2961  2rmorex  2970  cbvsbcw  3017  cbvsbc  3018  sbccomlem  3064  rmo3  3081  csbcow  3095  csbabg  3146  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  eqss  3198  uniiunlem  3272  ssequn1  3333  unss  3337  rexun  3343  ralunb  3344  elin3  3354  incom  3355  inass  3373  ssin  3385  ssddif  3397  unssdif  3398  difin  3400  invdif  3405  indif  3406  indi  3410  symdifxor  3429  disj3  3503  eldifpr  3649  rexsns  3661  reusn  3693  prss  3778  tpss  3788  eluni2  3843  elunirab  3852  uniun  3858  uni0b  3864  unissb  3869  elintrab  3886  ssintrab  3897  intun  3905  intpr  3906  iuncom  3922  iuncom4  3923  iunab  3963  ssiinf  3966  iinab  3978  iunin2  3980  iunun  3995  iunxun  3996  iunxiun  3998  sspwuni  4001  iinpw  4007  cbvdisj  4020  brun  4084  brin  4085  brdif  4086  dftr2  4133  inuni  4188  repizf2lem  4194  unidif0  4200  ssext  4254  pweqb  4256  otth2  4274  opelopabsbALT  4293  eqopab2b  4314  pwin  4317  unisuc  4448  elpwpwel  4510  sucexb  4533  elomssom  4641  xpiundi  4721  xpiundir  4722  poinxp  4732  soinxp  4733  seinxp  4734  inopab  4798  difopab  4799  raliunxp  4807  rexiunxp  4808  iunxpf  4814  cnvco  4851  dmiun  4875  dmuni  4876  dm0rn0  4883  brres  4952  dmres  4967  restidsing  5002  cnvsym  5053  asymref  5055  codir  5058  qfto  5059  cnvopab  5071  cnvdif  5076  rniun  5080  dminss  5084  imainss  5085  cnvcnvsn  5146  resco  5174  imaco  5175  rnco  5176  coiun  5179  coass  5188  ressn  5210  cnviinm  5211  xpcom  5216  funcnv  5319  funcnv3  5320  fncnv  5324  fun11  5325  fnres  5374  dfmpt3  5380  fnopabg  5381  fintm  5443  fin  5444  fores  5490  dff1o3  5510  fun11iun  5525  f11o  5537  f1ompt  5713  fsn  5734  imaiun  5807  isores2  5860  eqoprab2b  5980  opabex3d  6178  opabex3  6179  dfopab2  6247  dfoprab3s  6248  fmpox  6258  tpostpos  6322  dfsmo2  6345  qsid  6659  mapval2  6737  mapsncnv  6754  elixp2  6761  ixpin  6782  xpassen  6889  diffitest  6948  pw1dc0el  6972  supmoti  7059  eqinfti  7086  distrnqg  7454  ltbtwnnq  7483  distrnq0  7526  nqprrnd  7610  ltresr  7906  elznn0nn  9340  xrnemnf  9852  xrnepnf  9853  elioomnf  10043  elxrge0  10053  elfzuzb  10094  fzass4  10137  elfz2nn0  10187  elfzo2  10225  elfzo3  10239  lbfzo0  10257  fzind2  10315  infssuzex  10323  dfrp2  10353  rexfiuz  11154  fisumcom2  11603  prodmodc  11743  fprodcom2fi  11791  4sqlem12  12571  infpn2  12673  xpsfrnel  12987  xpscf  12990  islmod  13847  isbasis2g  14281  tgval2  14287  ntreq0  14368  txuni2  14492  isms2  14690  plyun0  14972  bdceq  15488