Theorem 3bitr4i 211

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

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi2d  231  pm4.71  386  pm5.32ri  450  mpan10  465  an31  553  an4  575  or4  760  ordir  806  andir  808  3anrot  967  3orrot  968  3ancoma  969  3orcomb  971  3ioran  977  3anbi123i  1170  3orbi123i  1171  3or6  1301  xorcom  1366  nfbii  1449  19.26-3an  1459  alnex  1475  19.42h  1665  19.42  1666  equsal  1705  sb6  1858  eeeanv  1905  sbbi  1932  sbco3xzyz  1946  sbcom2v  1960  sbel2x  1973  sb8eu  2012  sb8mo  2013  sb8euh  2022  eu1  2024  cbvmo  2039  mo3h  2052  sbmo  2058  eqcom  2141  abeq1  2249  cbvabw  2262  cbvab  2263  clelab  2265  nfceqi  2277  sbabel  2307  ralbii2  2445  rexbii2  2446  r2alf  2452  r2exf  2453  nfraldya  2469  nfrexdya  2470  r3al  2477  r19.41  2586  r19.42v  2588  ralcomf  2592  rexcomf  2593  reean  2599  3reeanv  2601  rabid2  2607  rabbi  2608  reubiia  2615  rmobiia  2620  reu5  2643  rmo5  2646  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvrmo  2653  vjust  2687  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  eueq  2855  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  rmo3f  2881  2rmorex  2890  cbvsbcw  2936  cbvsbc  2937  sbccomlem  2983  rmo3  3000  csbabg  3061  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  eqss  3112  uniiunlem  3185  ssequn1  3246  unss  3250  rexun  3256  ralunb  3257  elin3  3267  incom  3268  inass  3286  ssin  3298  ssddif  3310  unssdif  3311  difin  3313  invdif  3318  indif  3319  indi  3323  symdifxor  3342  disj3  3415  rexsns  3563  reusn  3594  prss  3676  tpss  3685  eluni2  3740  elunirab  3749  uniun  3755  uni0b  3761  unissb  3766  elintrab  3783  ssintrab  3794  intun  3802  intpr  3803  iuncom  3819  iuncom4  3820  iunab  3859  ssiinf  3862  iinab  3874  iunin2  3876  iunun  3891  iunxun  3892  iunxiun  3894  sspwuni  3897  iinpw  3903  cbvdisj  3916  brun  3979  brin  3980  brdif  3981  dftr2  4028  inuni  4080  repizf2lem  4085  unidif0  4091  ssext  4143  pweqb  4145  otth2  4163  opelopabsbALT  4181  eqopab2b  4201  pwin  4204  unisuc  4335  elpwpwel  4396  sucexb  4413  elnn  4519  xpiundi  4597  xpiundir  4598  poinxp  4608  soinxp  4609  seinxp  4610  inopab  4671  difopab  4672  raliunxp  4680  rexiunxp  4681  iunxpf  4687  cnvco  4724  dmiun  4748  dmuni  4749  dm0rn0  4756  brres  4825  dmres  4840  cnvsym  4922  asymref  4924  codir  4927  qfto  4928  cnvopab  4940  cnvdif  4945  rniun  4949  dminss  4953  imainss  4954  cnvcnvsn  5015  resco  5043  imaco  5044  rnco  5045  coiun  5048  coass  5057  ressn  5079  cnviinm  5080  xpcom  5085  funcnv  5184  funcnv3  5185  fncnv  5189  fun11  5190  fnres  5239  dfmpt3  5245  fnopabg  5246  fintm  5308  fin  5309  fores  5354  dff1o3  5373  fun11iun  5388  f11o  5400  f1ompt  5571  fsn  5592  imaiun  5661  isores2  5714  eqoprab2b  5829  opabex3d  6019  opabex3  6020  dfopab2  6087  dfoprab3s  6088  fmpox  6098  tpostpos  6161  dfsmo2  6184  qsid  6494  mapval2  6572  mapsncnv  6589  elixp2  6596  ixpin  6617  xpassen  6724  diffitest  6781  supmoti  6880  eqinfti  6907  distrnqg  7195  ltbtwnnq  7224  distrnq0  7267  nqprrnd  7351  ltresr  7647  elznn0nn  9068  xrnemnf  9564  xrnepnf  9565  elioomnf  9751  elxrge0  9761  elfzuzb  9800  fzass4  9842  elfz2nn0  9892  elfzo2  9927  elfzo3  9940  lbfzo0  9958  fzind2  10016  rexfiuz  10761  fisumcom2  11207  prodmodc  11347  infssuzex  11642  isbasis2g  12212  tgval2  12220  ntreq0  12301  txuni2  12425  isms2  12623  bdceq  13040