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  566  an4  588  or4  779  ordir  825  andir  827  3anrot  1010  3orrot  1011  3ancoma  1012  3orcomb  1014  3ioran  1020  3anbi123i  1215  3orbi123i  1216  3or6  1360  xorcom  1433  nfbii  1522  19.26-3an  1532  alnex  1548  19.42h  1735  19.42  1736  equsal  1775  equsalv  1842  sb6  1937  eeeanv  1989  sbbi  2015  sbco3xzyz  2029  sbcom2v  2041  sbel2x  2054  sb8eu  2095  sb8mo  2096  sb8euh  2105  eu1  2107  cbvmo  2122  mo3h  2136  sbmo  2142  eqcom  2236  abeq1  2344  cbvabw  2359  cbvab  2360  clelab  2362  eqabcb  2371  nfceqi  2382  sbabel  2413  ralbii2  2554  rexbii2  2555  r2alf  2561  r2exf  2562  nfraldya  2579  nfrexdya  2580  r3al  2588  r19.41  2700  r19.42v  2702  ralcomf  2706  rexcomf  2707  reean  2714  3reeanv  2716  rabid2  2723  rabbi  2724  cbvrmow  2729  reubiia  2732  rmobiia  2737  reu5  2764  rmo5  2767  cbvralfw  2769  cbvrexfw  2770  cbvralf  2771  cbvrexf  2772  cbvreuw  2775  cbvreu  2778  cbvrmo  2779  cbvralvw  2784  cbvrexvw  2785  vjust  2816  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  eueq  2990  reu2  3007  reu6  3008  reu3  3009  rmo4  3012  rmo3f  3016  2rmorex  3025  cbvsbcw  3072  cbvsbc  3073  sbccomlem  3119  rmo3  3137  csbcow  3151  csbabg  3202  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  eqss  3255  uniiunlem  3330  ssequn1  3391  unss  3395  rexun  3401  ralunb  3402  elin3  3412  incom  3413  inass  3433  ssin  3445  ssddif  3457  unssdif  3458  difin  3460  invdif  3465  indif  3466  indi  3470  symdifxor  3489  disj3  3563  eldifpr  3718  rexsns  3730  reusn  3764  prss  3852  tpss  3864  eluni2  3920  elunirab  3929  uniun  3935  uni0b  3941  unissb  3946  elintrab  3963  ssintrab  3974  intun  3982  intpr  3983  iuncom  3999  iuncom4  4000  iunab  4040  ssiinf  4043  iinab  4055  iunin2  4057  iunun  4072  iunxun  4073  iunxiun  4075  sspwuni  4078  iinpw  4084  cbvdisj  4097  brun  4163  brin  4164  brdif  4165  dftr2  4212  inuni  4269  repizf2lem  4276  unidif0  4282  ssext  4339  pweqb  4341  otth2  4359  opelopabsbALT  4379  eqopab2b  4400  pwin  4405  unisuc  4536  elpwpwel  4598  sucexb  4621  elomssom  4729  xpiundi  4810  xpiundir  4811  poinxp  4821  soinxp  4822  seinxp  4823  inopab  4889  difopab  4890  raliunxp  4898  rexiunxp  4899  iunxpf  4905  cnvco  4942  dmiun  4967  dmuni  4968  dm0rn0  4975  brres  5046  dmres  5061  restidsing  5096  cnvsym  5148  asymref  5150  codir  5153  qfto  5154  cnvopab  5166  cnvdif  5171  rniun  5175  dminss  5179  imainss  5180  cnvcnvsn  5241  resco  5269  imaco  5270  rnco  5271  coiun  5274  coass  5283  ressn  5305  cnviinm  5306  xpcom  5311  funcnv  5419  funcnv3  5420  fncnv  5424  fun11  5425  fnres  5477  dfmpt3  5483  fnopabg  5484  fintm  5554  fin  5555  fores  5602  dff1o3  5622  fun11iun  5637  f11o  5650  f1ompt  5830  fsn  5851  imaiun  5935  isores2  5988  eqoprab2b  6113  opabex3d  6316  opabex3  6317  dfopab2  6385  dfoprab3s  6386  fmpox  6398  tpostpos  6497  dfsmo2  6520  qsid  6836  mapval2  6914  mapsncnv  6932  elixp2  6939  ixpin  6960  xpassen  7083  diffitest  7146  pw1dc0el  7173  supmoti  7286  eqinfti  7313  distrnqg  7704  ltbtwnnq  7733  distrnq0  7776  nqprrnd  7860  ltresr  8156  elznn0nn  9593  xrnemnf  10113  xrnepnf  10114  elioomnf  10304  elxrge0  10314  elfzuzb  10356  fzass4  10399  elfz2nn0  10450  elfzo2  10488  elfzo3  10502  lbfzo0  10523  fzind2  10589  infssuzex  10597  dfrp2  10627  rexfiuz  11678  fisumcom2  12128  prodmodc  12268  fprodcom2fi  12316  4sqlem12  13104  ballotfilemelo  13145  ballotfilem2  13149  infpn2  13224  xpsfrnel  13574  xpscf  13577  islmod  14456  isbasis2g  14927  tgval2  14933  ntreq0  15014  txuni2  15138  isms2  15336  plyun0  15618  bdceq  16629