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	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 187	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 184	1 ⊢ (𝜒 ↔ 𝜃)

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  1471  19.26-3an  1481  alnex  1497  19.42h  1685  19.42  1686  equsal  1725  equsalv  1791  sb6  1884  eeeanv  1931  sbbi  1957  sbco3xzyz  1971  sbcom2v  1983  sbel2x  1996  sb8eu  2037  sb8mo  2038  sb8euh  2047  eu1  2049  cbvmo  2064  mo3h  2077  sbmo  2083  eqcom  2177  abeq1  2285  cbvabw  2298  cbvab  2299  clelab  2301  nfceqi  2313  sbabel  2344  ralbii2  2485  rexbii2  2486  r2alf  2492  r2exf  2493  nfraldya  2510  nfrexdya  2511  r3al  2519  r19.41  2630  r19.42v  2632  ralcomf  2636  rexcomf  2637  reean  2643  3reeanv  2645  rabid2  2651  rabbi  2652  reubiia  2659  rmobiia  2664  reu5  2687  rmo5  2690  cbvralfw  2692  cbvrexfw  2693  cbvralf  2694  cbvrexf  2695  cbvreu  2699  cbvrmo  2700  cbvralvw  2705  cbvrexvw  2706  vjust  2736  ceqsex3v  2777  ceqsex4v  2778  ceqsex8v  2780  eueq  2906  reu2  2923  reu6  2924  reu3  2925  rmo4  2928  rmo3f  2932  2rmorex  2941  cbvsbcw  2988  cbvsbc  2989  sbccomlem  3035  rmo3  3052  csbcow  3066  csbabg  3116  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  eqss  3168  uniiunlem  3242  ssequn1  3303  unss  3307  rexun  3313  ralunb  3314  elin3  3324  incom  3325  inass  3343  ssin  3355  ssddif  3367  unssdif  3368  difin  3370  invdif  3375  indif  3376  indi  3380  symdifxor  3399  disj3  3473  eldifpr  3616  rexsns  3628  reusn  3660  prss  3745  tpss  3754  eluni2  3809  elunirab  3818  uniun  3824  uni0b  3830  unissb  3835  elintrab  3852  ssintrab  3863  intun  3871  intpr  3872  iuncom  3888  iuncom4  3889  iunab  3928  ssiinf  3931  iinab  3943  iunin2  3945  iunun  3960  iunxun  3961  iunxiun  3963  sspwuni  3966  iinpw  3972  cbvdisj  3985  brun  4049  brin  4050  brdif  4051  dftr2  4098  inuni  4150  repizf2lem  4156  unidif0  4162  ssext  4215  pweqb  4217  otth2  4235  opelopabsbALT  4253  eqopab2b  4273  pwin  4276  unisuc  4407  elpwpwel  4469  sucexb  4490  elomssom  4598  xpiundi  4678  xpiundir  4679  poinxp  4689  soinxp  4690  seinxp  4691  inopab  4752  difopab  4753  raliunxp  4761  rexiunxp  4762  iunxpf  4768  cnvco  4805  dmiun  4829  dmuni  4830  dm0rn0  4837  brres  4906  dmres  4921  restidsing  4956  cnvsym  5004  asymref  5006  codir  5009  qfto  5010  cnvopab  5022  cnvdif  5027  rniun  5031  dminss  5035  imainss  5036  cnvcnvsn  5097  resco  5125  imaco  5126  rnco  5127  coiun  5130  coass  5139  ressn  5161  cnviinm  5162  xpcom  5167  funcnv  5269  funcnv3  5270  fncnv  5274  fun11  5275  fnres  5324  dfmpt3  5330  fnopabg  5331  fintm  5393  fin  5394  fores  5439  dff1o3  5459  fun11iun  5474  f11o  5486  f1ompt  5659  fsn  5680  imaiun  5751  isores2  5804  eqoprab2b  5923  opabex3d  6112  opabex3  6113  dfopab2  6180  dfoprab3s  6181  fmpox  6191  tpostpos  6255  dfsmo2  6278  qsid  6590  mapval2  6668  mapsncnv  6685  elixp2  6692  ixpin  6713  xpassen  6820  diffitest  6877  pw1dc0el  6901  supmoti  6982  eqinfti  7009  distrnqg  7361  ltbtwnnq  7390  distrnq0  7433  nqprrnd  7517  ltresr  7813  elznn0nn  9240  xrnemnf  9748  xrnepnf  9749  elioomnf  9939  elxrge0  9949  elfzuzb  9989  fzass4  10032  elfz2nn0  10082  elfzo2  10120  elfzo3  10133  lbfzo0  10151  fzind2  10209  dfrp2  10234  rexfiuz  10966  fisumcom2  11414  prodmodc  11554  fprodcom2fi  11602  infssuzex  11917  infpn2  12424  isbasis2g  13123  tgval2  13131  ntreq0  13212  txuni2  13336  isms2  13534  bdceq  14163