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  773  ordir  819  andir  821  3anrot  986  3orrot  987  3ancoma  988  3orcomb  990  3ioran  996  3anbi123i  1191  3orbi123i  1192  3or6  1336  xorcom  1408  nfbii  1497  19.26-3an  1507  alnex  1523  19.42h  1711  19.42  1712  equsal  1751  equsalv  1817  sb6  1911  eeeanv  1962  sbbi  1988  sbco3xzyz  2002  sbcom2v  2014  sbel2x  2027  sb8eu  2068  sb8mo  2069  sb8euh  2078  eu1  2080  cbvmo  2095  mo3h  2109  sbmo  2115  eqcom  2209  abeq1  2317  cbvabw  2330  cbvab  2331  clelab  2333  nfceqi  2346  sbabel  2377  ralbii2  2518  rexbii2  2519  r2alf  2525  r2exf  2526  nfraldya  2543  nfrexdya  2544  r3al  2552  r19.41  2663  r19.42v  2665  ralcomf  2669  rexcomf  2670  reean  2677  3reeanv  2679  rabid2  2685  rabbi  2686  cbvrmow  2691  reubiia  2694  rmobiia  2699  reu5  2726  rmo5  2729  cbvralfw  2731  cbvrexfw  2732  cbvralf  2733  cbvrexf  2734  cbvreuw  2737  cbvreu  2740  cbvrmo  2741  cbvralvw  2746  cbvrexvw  2747  vjust  2777  ceqsex3v  2820  ceqsex4v  2821  ceqsex8v  2823  eueq  2951  reu2  2968  reu6  2969  reu3  2970  rmo4  2973  rmo3f  2977  2rmorex  2986  cbvsbcw  3033  cbvsbc  3034  sbccomlem  3080  rmo3  3098  csbcow  3112  csbabg  3163  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  eqss  3216  uniiunlem  3290  ssequn1  3351  unss  3355  rexun  3361  ralunb  3362  elin3  3372  incom  3373  inass  3391  ssin  3403  ssddif  3415  unssdif  3416  difin  3418  invdif  3423  indif  3424  indi  3428  symdifxor  3447  disj3  3521  eldifpr  3670  rexsns  3682  reusn  3714  prss  3800  tpss  3812  eluni2  3868  elunirab  3877  uniun  3883  uni0b  3889  unissb  3894  elintrab  3911  ssintrab  3922  intun  3930  intpr  3931  iuncom  3947  iuncom4  3948  iunab  3988  ssiinf  3991  iinab  4003  iunin2  4005  iunun  4020  iunxun  4021  iunxiun  4023  sspwuni  4026  iinpw  4032  cbvdisj  4045  brun  4111  brin  4112  brdif  4113  dftr2  4160  inuni  4215  repizf2lem  4221  unidif0  4227  ssext  4283  pweqb  4285  otth2  4303  opelopabsbALT  4323  eqopab2b  4344  pwin  4347  unisuc  4478  elpwpwel  4540  sucexb  4563  elomssom  4671  xpiundi  4751  xpiundir  4752  poinxp  4762  soinxp  4763  seinxp  4764  inopab  4828  difopab  4829  raliunxp  4837  rexiunxp  4838  iunxpf  4844  cnvco  4881  dmiun  4906  dmuni  4907  dm0rn0  4914  brres  4984  dmres  4999  restidsing  5034  cnvsym  5085  asymref  5087  codir  5090  qfto  5091  cnvopab  5103  cnvdif  5108  rniun  5112  dminss  5116  imainss  5117  cnvcnvsn  5178  resco  5206  imaco  5207  rnco  5208  coiun  5211  coass  5220  ressn  5242  cnviinm  5243  xpcom  5248  funcnv  5354  funcnv3  5355  fncnv  5359  fun11  5360  fnres  5412  dfmpt3  5418  fnopabg  5419  fintm  5483  fin  5484  fores  5530  dff1o3  5550  fun11iun  5565  f11o  5577  f1ompt  5754  fsn  5775  imaiun  5852  isores2  5905  eqoprab2b  6026  opabex3d  6229  opabex3  6230  dfopab2  6298  dfoprab3s  6299  fmpox  6309  tpostpos  6373  dfsmo2  6396  qsid  6710  mapval2  6788  mapsncnv  6805  elixp2  6812  ixpin  6833  xpassen  6950  diffitest  7010  pw1dc0el  7034  supmoti  7121  eqinfti  7148  distrnqg  7535  ltbtwnnq  7564  distrnq0  7607  nqprrnd  7691  ltresr  7987  elznn0nn  9421  xrnemnf  9934  xrnepnf  9935  elioomnf  10125  elxrge0  10135  elfzuzb  10176  fzass4  10219  elfz2nn0  10269  elfzo2  10307  elfzo3  10321  lbfzo0  10342  fzind2  10405  infssuzex  10413  dfrp2  10443  rexfiuz  11415  fisumcom2  11864  prodmodc  12004  fprodcom2fi  12052  4sqlem12  12840  infpn2  12942  xpsfrnel  13291  xpscf  13294  islmod  14168  isbasis2g  14632  tgval2  14638  ntreq0  14719  txuni2  14843  isms2  15041  plyun0  15323  bdceq  15977