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  1473  19.26-3an  1483  alnex  1499  19.42h  1687  19.42  1688  equsal  1727  equsalv  1793  sb6  1886  eeeanv  1933  sbbi  1959  sbco3xzyz  1973  sbcom2v  1985  sbel2x  1998  sb8eu  2039  sb8mo  2040  sb8euh  2049  eu1  2051  cbvmo  2066  mo3h  2079  sbmo  2085  eqcom  2179  abeq1  2287  cbvabw  2300  cbvab  2301  clelab  2303  nfceqi  2315  sbabel  2346  ralbii2  2487  rexbii2  2488  r2alf  2494  r2exf  2495  nfraldya  2512  nfrexdya  2513  r3al  2521  r19.41  2632  r19.42v  2634  ralcomf  2638  rexcomf  2639  reean  2646  3reeanv  2648  rabid2  2654  rabbi  2655  reubiia  2662  rmobiia  2667  reu5  2690  rmo5  2693  cbvralfw  2695  cbvrexfw  2696  cbvralf  2697  cbvrexf  2698  cbvreu  2702  cbvrmo  2703  cbvralvw  2708  cbvrexvw  2709  vjust  2739  ceqsex3v  2780  ceqsex4v  2781  ceqsex8v  2783  eueq  2909  reu2  2926  reu6  2927  reu3  2928  rmo4  2931  rmo3f  2935  2rmorex  2944  cbvsbcw  2991  cbvsbc  2992  sbccomlem  3038  rmo3  3055  csbcow  3069  csbabg  3119  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  eqss  3171  uniiunlem  3245  ssequn1  3306  unss  3310  rexun  3316  ralunb  3317  elin3  3327  incom  3328  inass  3346  ssin  3358  ssddif  3370  unssdif  3371  difin  3373  invdif  3378  indif  3379  indi  3383  symdifxor  3402  disj3  3476  eldifpr  3620  rexsns  3632  reusn  3664  prss  3749  tpss  3759  eluni2  3814  elunirab  3823  uniun  3829  uni0b  3835  unissb  3840  elintrab  3857  ssintrab  3868  intun  3876  intpr  3877  iuncom  3893  iuncom4  3894  iunab  3934  ssiinf  3937  iinab  3949  iunin2  3951  iunun  3966  iunxun  3967  iunxiun  3969  sspwuni  3972  iinpw  3978  cbvdisj  3991  brun  4055  brin  4056  brdif  4057  dftr2  4104  inuni  4156  repizf2lem  4162  unidif0  4168  ssext  4222  pweqb  4224  otth2  4242  opelopabsbALT  4260  eqopab2b  4280  pwin  4283  unisuc  4414  elpwpwel  4476  sucexb  4497  elomssom  4605  xpiundi  4685  xpiundir  4686  poinxp  4696  soinxp  4697  seinxp  4698  inopab  4760  difopab  4761  raliunxp  4769  rexiunxp  4770  iunxpf  4776  cnvco  4813  dmiun  4837  dmuni  4838  dm0rn0  4845  brres  4914  dmres  4929  restidsing  4964  cnvsym  5013  asymref  5015  codir  5018  qfto  5019  cnvopab  5031  cnvdif  5036  rniun  5040  dminss  5044  imainss  5045  cnvcnvsn  5106  resco  5134  imaco  5135  rnco  5136  coiun  5139  coass  5148  ressn  5170  cnviinm  5171  xpcom  5176  funcnv  5278  funcnv3  5279  fncnv  5283  fun11  5284  fnres  5333  dfmpt3  5339  fnopabg  5340  fintm  5402  fin  5403  fores  5448  dff1o3  5468  fun11iun  5483  f11o  5495  f1ompt  5668  fsn  5689  imaiun  5761  isores2  5814  eqoprab2b  5933  opabex3d  6122  opabex3  6123  dfopab2  6190  dfoprab3s  6191  fmpox  6201  tpostpos  6265  dfsmo2  6288  qsid  6600  mapval2  6678  mapsncnv  6695  elixp2  6702  ixpin  6723  xpassen  6830  diffitest  6887  pw1dc0el  6911  supmoti  6992  eqinfti  7019  distrnqg  7386  ltbtwnnq  7415  distrnq0  7458  nqprrnd  7542  ltresr  7838  elznn0nn  9267  xrnemnf  9777  xrnepnf  9778  elioomnf  9968  elxrge0  9978  elfzuzb  10019  fzass4  10062  elfz2nn0  10112  elfzo2  10150  elfzo3  10163  lbfzo0  10181  fzind2  10239  dfrp2  10264  rexfiuz  10998  fisumcom2  11446  prodmodc  11586  fprodcom2fi  11634  infssuzex  11950  infpn2  12457  xpsfrnel  12763  xpscf  12766  islmod  13381  isbasis2g  13548  tgval2  13554  ntreq0  13635  txuni2  13759  isms2  13957  bdceq  14597