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  1496  19.26-3an  1506  alnex  1522  19.42h  1710  19.42  1711  equsal  1750  equsalv  1816  sb6  1910  eeeanv  1961  sbbi  1987  sbco3xzyz  2001  sbcom2v  2013  sbel2x  2026  sb8eu  2067  sb8mo  2068  sb8euh  2077  eu1  2079  cbvmo  2094  mo3h  2107  sbmo  2113  eqcom  2207  abeq1  2315  cbvabw  2328  cbvab  2329  clelab  2331  nfceqi  2344  sbabel  2375  ralbii2  2516  rexbii2  2517  r2alf  2523  r2exf  2524  nfraldya  2541  nfrexdya  2542  r3al  2550  r19.41  2661  r19.42v  2663  ralcomf  2667  rexcomf  2668  reean  2675  3reeanv  2677  rabid2  2683  rabbi  2684  reubiia  2691  rmobiia  2696  reu5  2723  rmo5  2726  cbvralfw  2728  cbvrexfw  2729  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvrmo  2737  cbvralvw  2742  cbvrexvw  2743  vjust  2773  ceqsex3v  2815  ceqsex4v  2816  ceqsex8v  2818  eueq  2944  reu2  2961  reu6  2962  reu3  2963  rmo4  2966  rmo3f  2970  2rmorex  2979  cbvsbcw  3026  cbvsbc  3027  sbccomlem  3073  rmo3  3090  csbcow  3104  csbabg  3155  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  eqss  3208  uniiunlem  3282  ssequn1  3343  unss  3347  rexun  3353  ralunb  3354  elin3  3364  incom  3365  inass  3383  ssin  3395  ssddif  3407  unssdif  3408  difin  3410  invdif  3415  indif  3416  indi  3420  symdifxor  3439  disj3  3513  eldifpr  3660  rexsns  3672  reusn  3704  prss  3789  tpss  3799  eluni2  3854  elunirab  3863  uniun  3869  uni0b  3875  unissb  3880  elintrab  3897  ssintrab  3908  intun  3916  intpr  3917  iuncom  3933  iuncom4  3934  iunab  3974  ssiinf  3977  iinab  3989  iunin2  3991  iunun  4006  iunxun  4007  iunxiun  4009  sspwuni  4012  iinpw  4018  cbvdisj  4031  brun  4095  brin  4096  brdif  4097  dftr2  4144  inuni  4199  repizf2lem  4205  unidif0  4211  ssext  4265  pweqb  4267  otth2  4285  opelopabsbALT  4305  eqopab2b  4326  pwin  4329  unisuc  4460  elpwpwel  4522  sucexb  4545  elomssom  4653  xpiundi  4733  xpiundir  4734  poinxp  4744  soinxp  4745  seinxp  4746  inopab  4810  difopab  4811  raliunxp  4819  rexiunxp  4820  iunxpf  4826  cnvco  4863  dmiun  4887  dmuni  4888  dm0rn0  4895  brres  4965  dmres  4980  restidsing  5015  cnvsym  5066  asymref  5068  codir  5071  qfto  5072  cnvopab  5084  cnvdif  5089  rniun  5093  dminss  5097  imainss  5098  cnvcnvsn  5159  resco  5187  imaco  5188  rnco  5189  coiun  5192  coass  5201  ressn  5223  cnviinm  5224  xpcom  5229  funcnv  5335  funcnv3  5336  fncnv  5340  fun11  5341  fnres  5392  dfmpt3  5398  fnopabg  5399  fintm  5461  fin  5462  fores  5508  dff1o3  5528  fun11iun  5543  f11o  5555  f1ompt  5731  fsn  5752  imaiun  5829  isores2  5882  eqoprab2b  6003  opabex3d  6206  opabex3  6207  dfopab2  6275  dfoprab3s  6276  fmpox  6286  tpostpos  6350  dfsmo2  6373  qsid  6687  mapval2  6765  mapsncnv  6782  elixp2  6789  ixpin  6810  xpassen  6925  diffitest  6984  pw1dc0el  7008  supmoti  7095  eqinfti  7122  distrnqg  7500  ltbtwnnq  7529  distrnq0  7572  nqprrnd  7656  ltresr  7952  elznn0nn  9386  xrnemnf  9899  xrnepnf  9900  elioomnf  10090  elxrge0  10100  elfzuzb  10141  fzass4  10184  elfz2nn0  10234  elfzo2  10272  elfzo3  10286  lbfzo0  10305  fzind2  10368  infssuzex  10376  dfrp2  10406  rexfiuz  11300  fisumcom2  11749  prodmodc  11889  fprodcom2fi  11937  4sqlem12  12725  infpn2  12827  xpsfrnel  13176  xpscf  13179  islmod  14053  isbasis2g  14517  tgval2  14523  ntreq0  14604  txuni2  14728  isms2  14926  plyun0  15208  bdceq  15778