Theorem 3bitr4i 211

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 186	. 2 |- ( ph <-> th )
5	1, 4	bitri 183	1 |- ( ch <-> th )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi2d  231  pm4.71  387  pm5.32ri  451  mpan10  466  an31  554  an4  576  or4  761  ordir  807  andir  809  3anrot  973  3orrot  974  3ancoma  975  3orcomb  977  3ioran  983  3anbi123i  1178  3orbi123i  1179  3or6  1313  xorcom  1378  nfbii  1461  19.26-3an  1471  alnex  1487  19.42h  1675  19.42  1676  equsal  1715  equsalv  1781  sb6  1874  eeeanv  1921  sbbi  1947  sbco3xzyz  1961  sbcom2v  1973  sbel2x  1986  sb8eu  2027  sb8mo  2028  sb8euh  2037  eu1  2039  cbvmo  2054  mo3h  2067  sbmo  2073  eqcom  2167  abeq1  2276  cbvabw  2289  cbvab  2290  clelab  2292  nfceqi  2304  sbabel  2335  ralbii2  2476  rexbii2  2477  r2alf  2483  r2exf  2484  nfraldya  2501  nfrexdya  2502  r3al  2510  r19.41  2621  r19.42v  2623  ralcomf  2627  rexcomf  2628  reean  2634  3reeanv  2636  rabid2  2642  rabbi  2643  reubiia  2650  rmobiia  2655  reu5  2678  rmo5  2681  cbvralfw  2683  cbvrexfw  2684  cbvralf  2685  cbvrexf  2686  cbvreu  2690  cbvrmo  2691  cbvralvw  2696  cbvrexvw  2697  vjust  2727  ceqsex3v  2768  ceqsex4v  2769  ceqsex8v  2771  eueq  2897  reu2  2914  reu6  2915  reu3  2916  rmo4  2919  rmo3f  2923  2rmorex  2932  cbvsbcw  2978  cbvsbc  2979  sbccomlem  3025  rmo3  3042  csbcow  3056  csbabg  3106  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  eqss  3157  uniiunlem  3231  ssequn1  3292  unss  3296  rexun  3302  ralunb  3303  elin3  3313  incom  3314  inass  3332  ssin  3344  ssddif  3356  unssdif  3357  difin  3359  invdif  3364  indif  3365  indi  3369  symdifxor  3388  disj3  3461  eldifpr  3603  rexsns  3615  reusn  3647  prss  3729  tpss  3738  eluni2  3793  elunirab  3802  uniun  3808  uni0b  3814  unissb  3819  elintrab  3836  ssintrab  3847  intun  3855  intpr  3856  iuncom  3872  iuncom4  3873  iunab  3912  ssiinf  3915  iinab  3927  iunin2  3929  iunun  3944  iunxun  3945  iunxiun  3947  sspwuni  3950  iinpw  3956  cbvdisj  3969  brun  4033  brin  4034  brdif  4035  dftr2  4082  inuni  4134  repizf2lem  4140  unidif0  4146  ssext  4199  pweqb  4201  otth2  4219  opelopabsbALT  4237  eqopab2b  4257  pwin  4260  unisuc  4391  elpwpwel  4453  sucexb  4474  elomssom  4582  xpiundi  4662  xpiundir  4663  poinxp  4673  soinxp  4674  seinxp  4675  inopab  4736  difopab  4737  raliunxp  4745  rexiunxp  4746  iunxpf  4752  cnvco  4789  dmiun  4813  dmuni  4814  dm0rn0  4821  brres  4890  dmres  4905  cnvsym  4987  asymref  4989  codir  4992  qfto  4993  cnvopab  5005  cnvdif  5010  rniun  5014  dminss  5018  imainss  5019  cnvcnvsn  5080  resco  5108  imaco  5109  rnco  5110  coiun  5113  coass  5122  ressn  5144  cnviinm  5145  xpcom  5150  funcnv  5249  funcnv3  5250  fncnv  5254  fun11  5255  fnres  5304  dfmpt3  5310  fnopabg  5311  fintm  5373  fin  5374  fores  5419  dff1o3  5438  fun11iun  5453  f11o  5465  f1ompt  5636  fsn  5657  imaiun  5728  isores2  5781  eqoprab2b  5900  opabex3d  6089  opabex3  6090  dfopab2  6157  dfoprab3s  6158  fmpox  6168  tpostpos  6232  dfsmo2  6255  qsid  6566  mapval2  6644  mapsncnv  6661  elixp2  6668  ixpin  6689  xpassen  6796  diffitest  6853  pw1dc0el  6877  supmoti  6958  eqinfti  6985  distrnqg  7328  ltbtwnnq  7357  distrnq0  7400  nqprrnd  7484  ltresr  7780  elznn0nn  9205  xrnemnf  9713  xrnepnf  9714  elioomnf  9904  elxrge0  9914  elfzuzb  9954  fzass4  9997  elfz2nn0  10047  elfzo2  10085  elfzo3  10098  lbfzo0  10116  fzind2  10174  dfrp2  10199  rexfiuz  10931  fisumcom2  11379  prodmodc  11519  fprodcom2fi  11567  infssuzex  11882  infpn2  12389  isbasis2g  12683  tgval2  12691  ntreq0  12772  txuni2  12896  isms2  13094  bdceq  13724