Theorem 3bitr4i 210

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 185	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 182	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi2d  230  pm4.71  381  pm5.32ri  442  mpan10  457  an31  528  an4  550  or4  720  ordir  763  andir  765  dcbii  780  3anrot  924  3orrot  925  3ancoma  926  3orcomb  928  3ioran  934  3anbi123i  1127  3orbi123i  1128  3or6  1254  xorcom  1319  nfbii  1402  19.26-3an  1412  alnex  1428  19.42h  1617  19.42  1618  equsal  1655  sb6  1807  eeeanv  1849  sbbi  1874  sbco3xzyz  1888  sbcom2v  1902  sbel2x  1915  sb8eu  1954  sb8mo  1955  sb8euh  1964  eu1  1966  cbvmo  1981  mo3h  1994  sbmo  2000  eqcom  2083  abeq1  2188  cbvab  2201  clelab  2203  nfceqi  2215  sbabel  2244  ralbii2  2376  rexbii2  2377  r2alf  2383  r2exf  2384  nfraldya  2400  nfrexdya  2401  r3al  2408  r19.41  2509  r19.42v  2511  ralcomf  2515  rexcomf  2516  reean  2522  3reeanv  2524  rabid2  2530  rabbi  2531  reubiia  2538  rmobiia  2543  reu5  2566  rmo5  2569  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvrmo  2576  vjust  2602  ceqsex3v  2641  ceqsex4v  2642  ceqsex8v  2644  eueq  2763  reu2  2780  reu6  2781  reu3  2782  rmo4  2785  2rmorex  2796  cbvsbc  2842  sbccomlem  2888  rmo3  2905  csbabg  2963  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  eqss  3014  uniiunlem  3082  ssequn1  3142  unss  3146  rexun  3152  ralunb  3153  elin3  3157  incom  3158  inass  3176  ssin  3188  ssddif  3198  unssdif  3199  difin  3201  invdif  3206  indif  3207  indi  3211  symdifxor  3230  disj3  3296  rexsns  3432  reusn  3463  prss  3541  tpss  3550  eluni2  3605  elunirab  3614  uniun  3620  uni0b  3626  unissb  3631  elintrab  3648  ssintrab  3659  intun  3667  intpr  3668  iuncom  3684  iuncom4  3685  iunab  3724  ssiinf  3727  iinab  3739  iunin2  3741  iunun  3755  iunxun  3756  iunxiun  3757  sspwuni  3760  iinpw  3763  cbvdisj  3776  brun  3831  brin  3832  brdif  3833  dftr2  3877  inuni  3930  repizf2lem  3935  unidif0  3941  ssext  3976  pweqb  3978  otth2  3996  opelopabsbALT  4014  eqopab2b  4034  pwin  4037  unisuc  4168  sucexb  4241  elnn  4346  xpiundi  4416  xpiundir  4417  poinxp  4427  soinxp  4428  seinxp  4429  inopab  4486  difopab  4487  raliunxp  4495  rexiunxp  4496  iunxpf  4502  cnvco  4538  dmiun  4562  dmuni  4563  dm0rn0  4570  brres  4636  dmres  4650  cnvsym  4728  asymref  4730  codir  4733  qfto  4734  cnvopab  4746  cnvdif  4750  rniun  4754  dminss  4758  imainss  4759  cnvcnvsn  4817  resco  4845  imaco  4846  rnco  4847  coiun  4850  coass  4859  ressn  4878  cnviinm  4879  xpcom  4884  funcnv  4980  funcnv3  4981  fncnv  4985  fun11  4986  fnres  5035  dfmpt3  5041  fnopabg  5042  fintm  5095  fin  5096  fores  5135  dff1o3  5152  fun11iun  5167  f11o  5179  f1ompt  5341  fsn  5356  imaiun  5420  isores2  5473  eqoprab2b  5583  opabex3d  5768  opabex3  5769  dfopab2  5835  dfoprab3s  5836  fmpt2x  5846  tpostpos  5902  dfsmo2  5925  qsid  6194  xpassen  6327  diffitest  6371  supmoti  6406  eqinfti  6433  distrnqg  6577  ltbtwnnq  6606  distrnq0  6649  nqprrnd  6733  ltresr  7007  elznn0nn  8365  xrnemnf  8853  xrnepnf  8854  elioomnf  8991  elxrge0  9001  elfzuzb  9039  fzass4  9080  elfz2nn0  9128  elfzo2  9160  elfzo3  9172  lbfzo0  9190  fzind2  9248  rexfiuz  9875  infssuzex  10345  bdceq  10633