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  771  ordir  817  andir  819  3anrot  983  3orrot  984  3ancoma  985  3orcomb  987  3ioran  993  3anbi123i  1188  3orbi123i  1189  3or6  1323  xorcom  1388  nfbii  1473  19.26-3an  1483  alnex  1499  19.42h  1687  19.42  1688  equsal  1727  equsalv  1793  sb6  1886  eeeanv  1933  sbbi  1959  sbco3xzyz  1973  sbcom2v  1985  sbel2x  1998  sb8eu  2039  sb8mo  2040  sb8euh  2049  eu1  2051  cbvmo  2066  mo3h  2079  sbmo  2085  eqcom  2179  abeq1  2287  cbvabw  2300  cbvab  2301  clelab  2303  nfceqi  2315  sbabel  2346  ralbii2  2487  rexbii2  2488  r2alf  2494  r2exf  2495  nfraldya  2512  nfrexdya  2513  r3al  2521  r19.41  2632  r19.42v  2634  ralcomf  2638  rexcomf  2639  reean  2645  3reeanv  2647  rabid2  2653  rabbi  2654  reubiia  2661  rmobiia  2666  reu5  2689  rmo5  2692  cbvralfw  2694  cbvrexfw  2695  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrmo  2702  cbvralvw  2707  cbvrexvw  2708  vjust  2738  ceqsex3v  2779  ceqsex4v  2780  ceqsex8v  2782  eueq  2908  reu2  2925  reu6  2926  reu3  2927  rmo4  2930  rmo3f  2934  2rmorex  2943  cbvsbcw  2990  cbvsbc  2991  sbccomlem  3037  rmo3  3054  csbcow  3068  csbabg  3118  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  eqss  3170  uniiunlem  3244  ssequn1  3305  unss  3309  rexun  3315  ralunb  3316  elin3  3326  incom  3327  inass  3345  ssin  3357  ssddif  3369  unssdif  3370  difin  3372  invdif  3377  indif  3378  indi  3382  symdifxor  3401  disj3  3475  eldifpr  3619  rexsns  3631  reusn  3663  prss  3748  tpss  3757  eluni2  3812  elunirab  3821  uniun  3827  uni0b  3833  unissb  3838  elintrab  3855  ssintrab  3866  intun  3874  intpr  3875  iuncom  3891  iuncom4  3892  iunab  3931  ssiinf  3934  iinab  3946  iunin2  3948  iunun  3963  iunxun  3964  iunxiun  3966  sspwuni  3969  iinpw  3975  cbvdisj  3988  brun  4052  brin  4053  brdif  4054  dftr2  4101  inuni  4153  repizf2lem  4159  unidif0  4165  ssext  4219  pweqb  4221  otth2  4239  opelopabsbALT  4257  eqopab2b  4277  pwin  4280  unisuc  4411  elpwpwel  4473  sucexb  4494  elomssom  4602  xpiundi  4682  xpiundir  4683  poinxp  4693  soinxp  4694  seinxp  4695  inopab  4756  difopab  4757  raliunxp  4765  rexiunxp  4766  iunxpf  4772  cnvco  4809  dmiun  4833  dmuni  4834  dm0rn0  4841  brres  4910  dmres  4925  restidsing  4960  cnvsym  5009  asymref  5011  codir  5014  qfto  5015  cnvopab  5027  cnvdif  5032  rniun  5036  dminss  5040  imainss  5041  cnvcnvsn  5102  resco  5130  imaco  5131  rnco  5132  coiun  5135  coass  5144  ressn  5166  cnviinm  5167  xpcom  5172  funcnv  5274  funcnv3  5275  fncnv  5279  fun11  5280  fnres  5329  dfmpt3  5335  fnopabg  5336  fintm  5398  fin  5399  fores  5444  dff1o3  5464  fun11iun  5479  f11o  5491  f1ompt  5664  fsn  5685  imaiun  5756  isores2  5809  eqoprab2b  5928  opabex3d  6117  opabex3  6118  dfopab2  6185  dfoprab3s  6186  fmpox  6196  tpostpos  6260  dfsmo2  6283  qsid  6595  mapval2  6673  mapsncnv  6690  elixp2  6697  ixpin  6718  xpassen  6825  diffitest  6882  pw1dc0el  6906  supmoti  6987  eqinfti  7014  distrnqg  7381  ltbtwnnq  7410  distrnq0  7453  nqprrnd  7537  ltresr  7833  elznn0nn  9261  xrnemnf  9771  xrnepnf  9772  elioomnf  9962  elxrge0  9972  elfzuzb  10012  fzass4  10055  elfz2nn0  10105  elfzo2  10143  elfzo3  10156  lbfzo0  10174  fzind2  10232  dfrp2  10257  rexfiuz  10989  fisumcom2  11437  prodmodc  11577  fprodcom2fi  11625  infssuzex  11940  infpn2  12447  isbasis2g  13325  tgval2  13333  ntreq0  13414  txuni2  13538  isms2  13736  bdceq  14365