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  4182  brin  4183  brdif  4184  dftr2  4231  inuni  4291  repizf2lem  4298  unidif0  4304  ssext  4361  pweqb  4363  otth2  4381  opelopabsbALT  4401  eqopab2b  4422  pwin  4427  unisuc  4558  elpwpwel  4621  sucexb  4644  elomssom  4752  xpiundi  4833  xpiundir  4834  poinxp  4844  soinxp  4845  seinxp  4846  inopab  4912  difopab  4913  raliunxp  4921  rexiunxp  4922  iunxpf  4928  cnvco  4965  dmiun  4990  dmuni  4991  dm0rn0  4998  brres  5069  dmres  5084  restidsing  5119  cnvsym  5171  asymref  5173  codir  5176  qfto  5177  cnvopab  5189  cnvdif  5194  rniun  5198  dminss  5202  imainss  5203  cnvcnvsn  5264  resco  5292  imaco  5293  rnco  5294  coiun  5297  coass  5306  ressn  5328  cnviinm  5329  xpcom  5334  funcnv  5442  funcnv3  5443  fncnv  5447  fun11  5448  fnres  5500  dfmpt3  5506  fnopabg  5507  fintm  5577  fin  5578  fores  5625  dff1o3  5645  fun11iun  5660  f11o  5673  f1ompt  5859  fsn  5880  imaiun  5966  isores2  6019  eqoprab2b  6146  opabex3d  6350  opabex3  6351  dfopab2  6423  dfoprab3s  6424  fmpox  6436  tpostpos  6535  dfsmo2  6558  qsid  6874  mapval2  6959  mapsncnv  6977  elixp2  6984  ixpin  7005  xpassen  7128  diffitest  7191  pw1dc0el  7218  supmoti  7333  eqinfti  7360  distrnqg  7754  ltbtwnnq  7783  distrnq0  7826  nqprrnd  7910  ltresr  8206  elznn0nn  9658  xrnemnf  10179  xrnepnf  10180  elioomnf  10370  elxrge0  10380  elfzuzb  10422  fzass4  10468  elfz2nn0  10519  elfzo2  10557  elfzo3  10571  lbfzo0  10592  fzind2  10658  infssuzex  10666  dfrp2  10698  rexfiuz  11755  fisumcom2  12205  prodmodc  12345  fprodcom2fi  12393  4sqlem12  13181  ballotfilemelo  13222  ballotfilem2  13228  infpn2  13347  xpsfrnel  13665  xpscf  13668  drngprop  14617  opprdrng  14620  islmod  14627  isbasis2g  15146  tgval2  15152  ntreq0  15233  txuni2  15357  isms2  15555  plyun0  15837  bdceq  16868  dfrals2  17130  alsbii  17141  ralsbii  17142  cbvals  17146  dfralseu2  17164  alseubii  17173  ralseubii  17174