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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi2d  232  pm4.71  393  pm5.32ri  459  mpan10  478  an31  570  an4  592  or4  783  ordir  829  andir  831  3anrot  1014  3orrot  1015  3ancoma  1016  3orcomb  1018  3ioran  1024  3anbi123i  1219  3orbi123i  1220  3or6  1364  xorcom  1437  nfbii  1526  19.26-3an  1536  alnex  1552  19.42h  1739  19.42  1740  equsal  1779  equsalv  1846  sb6  1941  eeeanv  1993  sbbi  2019  sbco3xzyz  2033  sbcom2v  2045  sbel2x  2058  sb8eu  2099  sb8mo  2100  sb8euh  2109  eu1  2111  cbvmo  2126  mo3h  2140  sbmo  2146  eqcom  2240  abeq1  2348  cbvabw  2363  cbvab  2364  clelab  2366  eqabcbw  2376  eqabcb  2377  nfceqi  2388  sbabel  2419  ralbii2  2560  rexbii2  2561  r2alf  2567  r2exf  2568  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.41  2706  r19.42v  2708  ralcomf  2712  rexcomf  2713  reean  2720  3reeanv  2722  rabid2  2729  rabbi  2730  cbvrmow  2735  reubiia  2738  rmobiia  2743  reu5  2770  rmo5  2773  cbvralfw  2775  cbvrexfw  2776  cbvralf  2777  cbvrexf  2778  cbvreuw  2781  cbvreu  2784  cbvrmo  2785  cbvralvw  2790  cbvrexvw  2791  vjust  2822  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  eueq  2997  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  rmo3f  3023  2rmorex  3032  cbvsbcw  3079  cbvsbc  3080  sbccomlem  3126  rmo3  3144  csbcow  3158  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  eqss  3263  uniiunlem  3338  ssequn1  3399  unss  3403  rexun  3409  ralunb  3410  elin3  3420  incom  3421  inass  3441  ssin  3453  ssddif  3465  unssdif  3466  difin  3468  invdif  3473  indif  3474  indi  3478  symdifxor  3497  ab0w  3550  disj3  3577  eldifpr  3736  rexsns  3748  reusn  3782  prss  3871  tpss  3883  eluni2  3939  elunirab  3948  uniun  3954  uni0b  3960  unissb  3965  elintrab  3982  ssintrab  3993  intun  4001  intpr  4002  iuncom  4018  iuncom4  4019  iunab  4059  ssiinf  4062  iinab  4074  iunin2  4076  iunun  4091  iunxun  4092  iunxiun  4094  sspwuni  4097  iinpw  4103  cbvdisj  4116  brun  4183  brin  4184  brdif  4185  dftr2  4233  inuni  4293  repizf2lem  4300  unidif0  4306  ssext  4363  pweqb  4365  otth2  4383  opelopabsbALT  4403  eqopab2b  4424  pwin  4429  unisuc  4560  elpwpwel  4623  sucexb  4646  elomssom  4754  xpiundi  4835  xpiundir  4836  poinxp  4846  soinxp  4847  seinxp  4848  inopab  4914  difopab  4915  raliunxp  4923  rexiunxp  4924  iunxpf  4930  cnvco  4967  dmiun  4992  dmuni  4993  dm0rn0  5000  brres  5071  dmres  5086  restidsing  5122  cnvsym  5174  asymref  5176  codir  5179  qfto  5180  cnvopab  5192  cnvdif  5197  rniun  5201  dminss  5205  imainss  5206  cnvcnvsn  5267  resco  5295  imaco  5296  rnco  5297  coiun  5300  coass  5309  ressn  5331  cnviinm  5332  xpcom  5337  funcnv  5445  funcnv3  5446  fncnv  5450  fun11  5451  fnres  5503  dfmpt3  5509  fnopabg  5510  fintm  5580  fin  5581  fores  5628  dff1o3  5648  fun11iun  5663  f11o  5676  f1ompt  5862  fsn  5883  imaiun  5969  isores2  6022  eqoprab2b  6149  opabex3d  6354  opabex3  6355  dfopab2  6427  dfoprab3s  6428  fmpox  6440  tpostpos  6539  dfsmo2  6562  qsid  6878  mapval2  6963  mapsncnv  6981  elixp2  6988  ixpin  7009  xpassen  7132  diffitest  7195  pw1dc0el  7222  supmoti  7339  eqinfti  7366  distrnqg  7760  ltbtwnnq  7789  distrnq0  7832  nqprrnd  7916  ltresr  8212  elznn0nn  9669  xrnemnf  10196  xrnepnf  10197  elioomnf  10387  elxrge0  10397  elfzuzb  10439  fzass4  10485  elfz2nn0  10536  elfzo2  10574  elfzo3  10588  lbfzo0  10609  fzind2  10675  infssuzex  10683  dfrp2  10715  rexfiuz  11777  fisumcom2  12230  prodmodc  12370  fprodcom2fi  12418  4sqlem12  13210  ballotfilemelo  13280  ballotfilem2  13286  infpn2  13405  xpsfrnel  13724  xpscf  13727  drngprop  14726  opprdrng  14729  islmod  14736  isbasis2g  15271  tgval2  15277  ntreq0  15358  txuni2  15482  isms2  15680  plyun0  15962  bdceq  17073  dfrals2  17337  alsbii  17348  ralsbii  17349  cbvals  17353  dfralseu2  17371  alseubii  17380  ralseubii  17381