Theorem 3bitr4i 201

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

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi2d  221  pm4.71  369  pm5.32ri  428  mpan10  443  an31  498  an4  520  or4  688  ordir  730  andir  732  dcbii  747  3anrot  890  3orrot  891  3ancoma  892  3orcomb  894  3ioran  900  3anbi123i  1093  3orbi123i  1094  3or6  1218  xorcom  1279  nfbii  1362  19.26-3an  1372  alnex  1388  19.42h  1577  19.42  1578  equsal  1615  sb6  1766  eeeanv  1808  sbbi  1833  sbco3xzyz  1847  sbcom2v  1861  sbel2x  1874  sb8eu  1913  sb8mo  1914  sb8euh  1923  eu1  1925  cbvmo  1940  mo3h  1953  sbmo  1959  eqcom  2042  abeq1  2147  cbvab  2160  clelab  2162  nfceqi  2174  sbabel  2203  ralbii2  2334  rexbii2  2335  r2alf  2341  r2exf  2342  nfraldya  2358  nfrexdya  2359  r3al  2366  r19.41  2465  r19.42v  2467  ralcomf  2471  rexcomf  2472  reean  2478  3reeanv  2480  rabid2  2486  rabbi  2487  reubiia  2494  rmobiia  2499  reu5  2522  rmo5  2525  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvrmo  2532  vjust  2558  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  eueq  2712  reu2  2729  reu6  2730  reu3  2731  rmo4  2734  2rmorex  2745  cbvsbc  2791  sbccomlem  2832  rmo3  2849  csbabg  2907  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  eqss  2960  uniiunlem  3028  ssequn1  3113  unss  3117  rexun  3123  ralunb  3124  elin3  3128  incom  3129  inass  3147  ssin  3159  nssinpss  3169  ssddif  3171  unssdif  3172  difin  3174  invdif  3179  indif  3180  indi  3184  symdifxor  3203  disj3  3272  rexsns  3409  reusn  3441  difsnpssim  3507  prss  3520  tpss  3529  eluni2  3584  elunirab  3593  uniun  3599  uni0b  3605  unissb  3610  elintrab  3627  ssintrab  3638  intun  3646  intpr  3647  iuncom  3663  iuncom4  3664  iunab  3703  ssiinf  3706  iinab  3718  iunin2  3720  iunun  3734  iunxun  3735  iunxiun  3736  sspwuni  3739  iinpw  3742  cbvdisj  3755  brun  3810  brin  3811  brdif  3812  dftr2  3856  inuni  3909  repizf2lem  3914  unidif0  3920  ssext  3957  pweqb  3959  otth2  3978  opelopabsbALT  3996  eqopab2b  4016  pwin  4019  unisuc  4150  sucexb  4223  elnn  4328  xpiundi  4398  xpiundir  4399  poinxp  4409  soinxp  4410  seinxp  4411  inopab  4468  difopab  4469  raliunxp  4477  rexiunxp  4478  iunxpf  4484  cnvco  4520  dmiun  4544  dmuni  4545  dm0rn0  4552  brres  4618  dmres  4632  cnvsym  4708  asymref  4710  codir  4713  qfto  4714  cnvopab  4726  cnvdif  4730  rniun  4734  dminss  4738  imainss  4739  cnvcnvsn  4797  resco  4825  imaco  4826  rnco  4827  coiun  4830  coass  4839  ressn  4858  cnviinm  4859  xpcom  4864  funcnv  4960  funcnv3  4961  fncnv  4965  fun11  4966  fnres  5015  dfmpt3  5021  fnopabg  5022  fintm  5075  fin  5076  fores  5115  dff1o3  5132  fun11iun  5147  f11o  5159  f1ompt  5320  fsn  5335  imaiun  5399  isores2  5453  eqoprab2b  5563  opabex3d  5748  opabex3  5749  dfopab2  5815  dfoprab3s  5816  fmpt2x  5826  tpostpos  5879  dfsmo2  5902  qsid  6171  xpassen  6304  diffitest  6344  distrnqg  6485  ltbtwnnq  6514  distrnq0  6557  nqprrnd  6641  ltresr  6915  elznn0nn  8259  xrnemnf  8699  xrnepnf  8700  elioomnf  8837  elxrge0  8847  elfzuzb  8884  fzass4  8925  elfz2nn0  8973  elfzo2  9007  elfzo3  9019  lbfzo0  9037  fzind2  9095  bdceq  9962