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  968  3orrot  969  3ancoma  970  3orcomb  972  3ioran  978  3anbi123i  1171  3orbi123i  1172  3or6  1302  xorcom  1367  nfbii  1450  19.26-3an  1460  alnex  1476  19.42h  1666  19.42  1667  equsal  1706  sb6  1859  eeeanv  1906  sbbi  1933  sbco3xzyz  1947  sbcom2v  1961  sbel2x  1974  sb8eu  2013  sb8mo  2014  sb8euh  2023  eu1  2025  cbvmo  2040  mo3h  2053  sbmo  2059  eqcom  2142  abeq1  2250  cbvabw  2263  cbvab  2264  clelab  2266  nfceqi  2278  sbabel  2308  ralbii2  2448  rexbii2  2449  r2alf  2455  r2exf  2456  nfraldya  2472  nfrexdya  2473  r3al  2480  r19.41  2589  r19.42v  2591  ralcomf  2595  rexcomf  2596  reean  2602  3reeanv  2604  rabid2  2610  rabbi  2611  reubiia  2618  rmobiia  2623  reu5  2646  rmo5  2649  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvrmo  2656  vjust  2690  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  eueq  2859  reu2  2876  reu6  2877  reu3  2878  rmo4  2881  rmo3f  2885  2rmorex  2894  cbvsbcw  2940  cbvsbc  2941  sbccomlem  2987  rmo3  3004  csbabg  3066  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  eqss  3117  uniiunlem  3190  ssequn1  3251  unss  3255  rexun  3261  ralunb  3262  elin3  3272  incom  3273  inass  3291  ssin  3303  ssddif  3315  unssdif  3316  difin  3318  invdif  3323  indif  3324  indi  3328  symdifxor  3347  disj3  3420  eldifpr  3559  rexsns  3570  reusn  3602  prss  3684  tpss  3693  eluni2  3748  elunirab  3757  uniun  3763  uni0b  3769  unissb  3774  elintrab  3791  ssintrab  3802  intun  3810  intpr  3811  iuncom  3827  iuncom4  3828  iunab  3867  ssiinf  3870  iinab  3882  iunin2  3884  iunun  3899  iunxun  3900  iunxiun  3902  sspwuni  3905  iinpw  3911  cbvdisj  3924  brun  3987  brin  3988  brdif  3989  dftr2  4036  inuni  4088  repizf2lem  4093  unidif0  4099  ssext  4151  pweqb  4153  otth2  4171  opelopabsbALT  4189  eqopab2b  4209  pwin  4212  unisuc  4343  elpwpwel  4404  sucexb  4421  elnn  4527  xpiundi  4605  xpiundir  4606  poinxp  4616  soinxp  4617  seinxp  4618  inopab  4679  difopab  4680  raliunxp  4688  rexiunxp  4689  iunxpf  4695  cnvco  4732  dmiun  4756  dmuni  4757  dm0rn0  4764  brres  4833  dmres  4848  cnvsym  4930  asymref  4932  codir  4935  qfto  4936  cnvopab  4948  cnvdif  4953  rniun  4957  dminss  4961  imainss  4962  cnvcnvsn  5023  resco  5051  imaco  5052  rnco  5053  coiun  5056  coass  5065  ressn  5087  cnviinm  5088  xpcom  5093  funcnv  5192  funcnv3  5193  fncnv  5197  fun11  5198  fnres  5247  dfmpt3  5253  fnopabg  5254  fintm  5316  fin  5317  fores  5362  dff1o3  5381  fun11iun  5396  f11o  5408  f1ompt  5579  fsn  5600  imaiun  5669  isores2  5722  eqoprab2b  5837  opabex3d  6027  opabex3  6028  dfopab2  6095  dfoprab3s  6096  fmpox  6106  tpostpos  6169  dfsmo2  6192  qsid  6502  mapval2  6580  mapsncnv  6597  elixp2  6604  ixpin  6625  xpassen  6732  diffitest  6789  supmoti  6888  eqinfti  6915  distrnqg  7219  ltbtwnnq  7248  distrnq0  7291  nqprrnd  7375  ltresr  7671  elznn0nn  9092  xrnemnf  9594  xrnepnf  9595  elioomnf  9781  elxrge0  9791  elfzuzb  9831  fzass4  9873  elfz2nn0  9923  elfzo2  9958  elfzo3  9971  lbfzo0  9989  fzind2  10047  rexfiuz  10793  fisumcom2  11239  prodmodc  11379  infssuzex  11678  isbasis2g  12251  tgval2  12259  ntreq0  12340  txuni2  12464  isms2  12662  bdceq  13211