Theorem 3bitr4i 303

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, 3-Jan-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 278	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 275	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bibi2d  342  pm4.71  557  pm5.32ri  575  an31  649  pm4.14  807  or4  927  orimdi  931  orbidi  955  ordi  1008  ordir  1009  andir  1011  dfbi3  1050  dfifp7  1070  ifpdfbi  1071  ifpn  1074  3orrot  1092  3orcoma  1093  3ioran  1106  3ianor  1107  3anbi123i  1156  3orbi123i  1157  3jaob  1429  an6  1448  3or6  1450  an3andi  1485  an33rean  1486  nancom  1498  xorass  1517  anxordi  1528  norass  1539  hadbi  1600  hadcoma  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1676  19.26-3an  1874  19.43OLD  1885  19.32v  1942  19.31v  1943  19.42v  1955  4exdistr  1963  cbvexvw  2039  exexw  2055  sb3an  2087  sbcom4  2095  sbbiiev  2098  excom  2168  sbal  2175  19.32  2241  19.31  2242  19.42  2244  equsalv  2275  sbex  2288  sbrim  2311  sbor  2313  sbbi  2314  cbvex2v  2348  eeeanv  2354  sbnf2  2362  cbvsbvf  2367  cbvex2  2416  equsal  2421  dfsb3  2498  mo4  2566  eu6  2574  dfeu  2595  sb8eulem  2598  sb8mo  2601  cbvmovw  2602  cbvmow  2603  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  eu1  2610  sbmo  2614  cbvabv  2806  cbvabw  2807  cbvab  2808  eqabcbw  2810  eqabcb  2876  nfceqi  2895  ralbii2  3079  rexbii2  3080  r19.26-3  3098  r19.43  3105  r2allem  3125  r19.42v  3169  r19.32v  3170  reeanlem  3208  3reeanv  3210  cbvralvw  3215  cbvrexvw  3216  ralcom  3265  ralcomf  3275  rexcomf  3276  cbvralfw  3277  cbvralsvw  3288  cbvralf  3322  cbvrexf  3323  reu5  3344  rmobiia  3348  reubiia  3349  rmo5  3360  cbvrmovw  3363  cbvreuvw  3364  cbvrmow  3367  cbvreuw  3368  cbvreu  3381  cbvrmo  3382  rabid2f  3420  abv  3441  abvALT  3442  ceqsal  3467  ceqsalv  3469  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  reurab  3647  eueq  3654  reu2  3671  reu6  3672  reu3  3673  rmo4  3676  rmo3f  3680  2reu5  3704  cbvsbcw  3761  cbvsbcvw  3762  cbvsbc  3763  sbc3an  3793  sbccomlemOLD  3808  rmo3  3827  rmoanim  3832  rmoanimALT  3833  cbvralcsf  3879  cbvrexcsf  3880  cbvreucsf  3881  eqss  3937  uniiunlem  4027  sspsstri  4045  compleq  4092  ssequn1  4126  unss  4130  rexun  4136  ralunb  4137  elin3  4146  inass  4168  ssin  4179  elsymdif  4198  nssinpss  4207  dfun2  4210  difin  4212  indi  4224  indifdi  4234  difin2  4241  eq0  4290  ssdif0  4306  inn0f  4311  inssdif0  4314  ab0w  4319  ab0  4320  ab0orv  4323  abn0  4325  rabeq0w  4327  rabeq0  4328  disj3  4394  ssundif  4427  ralidmw  4456  dfif2  4468  eldifpr  4602  rexdifpr  4603  rexsns  4615  snprc  4661  reusn  4671  difsnpss  4752  tpss  4780  pwpr  4844  eluni2  4854  elunirab  4865  uniun  4873  unissb  4883  elintrab  4902  ssintrab  4913  intun  4922  iuncom  4941  iuncom4  4942  iunab  4994  ssiinf  4997  iunn0  5009  iinab  5010  iunin2  5013  iinun2  5015  iundif2  5016  iunun  5035  iunxun  5036  iunxiun  5039  sspwuni  5042  iinpw  5048  cbvdisj  5062  cbvdisjv  5063  disjor  5067  brun  5136  brin  5137  brdif  5138  dftr2  5194  dftr5  5196  intexrab  5288  inuni  5291  ssext  5406  pweqb  5408  otth2  5436  otthne  5439  propeqop  5461  vopelopabsb  5484  eqopab2bw  5503  eqopab2b  5507  pwin  5522  pwun  5524  dffr6  5587  elxp2  5655  otelxp  5675  xpiundi  5702  xpiundir  5703  poinxp  5712  soinxp  5713  frinxp  5714  seinxp  5715  weinxp  5716  reliun  5772  inopab  5785  difopab  5786  inxp  5787  raliunxp  5794  rexiunxp  5795  rexxpf  5802  iunxpf  5803  cnvco  5840  dmiun  5868  dmuni  5869  dm0rn0  5879  dm0rn0OLD  5880  dmres  5977  restidsing  6018  asymref  6079  codir  6083  qfto  6084  cnvopab  6100  cnvopabOLD  6101  cnvdif  6107  rniun  6111  dminss  6117  imainss  6118  difxp  6128  xpdifid  6132  dmsnn0  6171  cnvcnvsn  6183  cnvresima  6194  resco  6214  imaco  6215  rnco  6216  rncoOLD  6217  coiun  6221  coass  6230  ressn  6249  cnviin  6250  cnvpo  6251  cnvso  6252  xpco  6253  opreu2reurex  6258  dfpo2  6260  imaindm  6263  dflim2  6381  funcnv  6567  funcnv3  6568  fncnv  6571  fun11  6572  imadif  6582  fnres  6625  dfmpt3  6632  mptfnf  6633  fnopabg  6635  fint  6719  fin  6720  fores  6762  dff1o3  6786  f1ompt  7063  fsn  7088  imaiun  7200  isocnv2  7286  isocnv3  7287  isores2  7288  isomin  7292  eqoprab2bw  7437  eqoprab2b  7438  elpwpwel  7721  sucexb  7758  onsucb  7768  dflim4  7799  fiun  7896  f1iun  7897  f11o  7900  opabex3d  7918  opabex3rd  7919  opabex3  7920  dfopab2  8005  dfoprab3s  8006  fmpox  8020  fparlem1  8062  fparlem2  8063  tpostpos  8196  frrlem9  8244  dfsmo2  8287  brwitnlem  8442  oarec  8497  naddasslem1  8630  naddasslem2  8631  qsid  8728  uniinqs  8744  mapval2  8820  mapsncnv  8841  elixp2  8849  ixpin  8871  brsdom  8921  brdom2  8929  xpassen  9009  brsdom2  9039  unfilem1  9215  fiint  9237  dfsup2  9357  supmo  9365  eqinf  9398  infmo  9410  brttrcl2  9635  rankc1  9794  cp  9815  isinfcard  10014  aceq1  10039  aceq2  10041  dfac5lem3  10047  dfac10b  10062  dfac12a  10071  dffin7-2  10320  dfacfin7  10321  fin1a2lem6  10327  iunfo  10461  konigthlem  10491  axgroth6  10751  axgroth3  10754  sstskm  10765  ltexprlem1  10959  gt0srpr  11001  ltpsrpr  11032  map2psrpr  11033  ltresr  11063  fimaxre3  12102  sup3  12113  supaddc  12123  supmul1  12125  elnn0z  12537  elznn0nn  12538  zmin  12894  xrnemnf  13068  xrnepnf  13069  dfrp2  13347  elioomnf  13397  elxrge0  13410  elfzuzb  13472  fzass4  13516  elfz2nn0  13572  elfzo2  13616  elfzo3  13631  lbfzo0  13654  fzo1lb  13668  fzind2  13743  nn0opthlem1  14230  hashgt23el  14386  cotr2g  14938  rexfiuz  15310  fsumcom2  15736  prodmo  15901  fprodcom2  15949  sinltx  16156  divalglem4  16365  divalglem10  16371  4sqlem12  16927  imasleval  17505  xpsfrnel  17526  xpscf  17529  isssc  17787  isffth2  17885  ispos2  18281  issubmgm  18670  ismhm  18753  issubmndb  18773  nsgacs  19137  isgim  19237  oppgcntz  19339  f1omvdco3  19424  pmtrprfvalrn  19463  efgrelexlemb  19725  pgpfac1  20057  pgpfac  20061  issrg  20169  opprsubg  20332  opprunit  20357  isirred2  20401  opprirred  20402  opprnzrb  20498  isdomn2OLD  20689  opprdomnb  20694  isdomn4r  20696  drngprop  20721  opprdrng  20741  issdrg2  20772  isorng  20838  islss  20929  islbs  21071  unocv  21660  iunocv  21661  isbasis2g  22913  tgval2  22921  ntreq0  23042  isclo2  23053  cmpcov2  23355  is1stc2  23407  1stcelcls  23426  llyi  23439  unisngl  23492  txuni2  23530  xkobval  23551  hausdiag  23610  isfbas2  23800  elfg  23836  fbasrn  23849  fmfnfmlem3  23921  isfcls  23974  alexsubALTlem2  24013  istmd  24039  istgp  24042  istrg  24129  istdrg  24131  istdrg2  24143  isms2  24415  metuel2  24530  restmetu  24535  isngp  24561  isngp2  24562  isngp3  24563  elii1  24902  isncvsngp  25116  iscph  25137  isbn  25305  pmltpc  25417  ovolfcl  25433  finiunmbl  25511  iundisj  25515  dyaddisj  25563  vitalilem1  25575  ellimc3  25846  ig1pval3  26143  plyun0  26162  plydivex  26263  aannenlem2  26295  ellogrn  26523  atandm  26840  atandm3  26842  atans2  26895  elno3  27619  conway  27771  eqcuts2  27778  madeval2  27825  ons2ind  28267  tgjustf  28541  colinearalg  28979  axeuclid  29032  nbgrsym  29432  upgrtrls  29768  upgristrl  29769  dfpth2  29797  usgr2pth0  29833  iswwlks  29904  isclwwlk  30054  clwwlkneq0  30099  h2hlm  31051  issh  31279  chcon2i  31535  chcon1i  31536  chcon3i  31537  chnlei  31556  cmcm2i  31664  cmcm3i  31665  3oalem3  31735  pjdifnormii  31754  pjneli  31794  dfadj2  31956  cnvadj  31963  hhcno  31975  hhcnf  31976  eleigvec  32028  eleigvec2  32029  pjimai  32247  isst  32284  ishst  32285  cvnbtwn4  32360  chrelat4i  32444  2reucom  32549  reuxfrdf  32560  difrab2  32567  inpr0  32602  iunin1f  32627  disjnf  32640  cbvdisjf  32641  disjorf  32649  iundisjf  32659  disjexc  32663  xrdifh  32853  iundisjfi  32869  hashxpe  32880  pmtrprfv2  33149  xrnarchi  33245  isunit2  33301  prmidl0  33510  opprnsg  33544  ccfldextdgrr  33816  cmpcref  33994  ordtconnlem1  34068  isrrext  34144  cntnevol  34372  ddemeas  34380  omssubaddlem  34443  omssubadd  34444  eulerpartleme  34507  eulerpartlemv  34508  eulerpartlemt0  34513  eulerpartlemgvv  34520  eulerpartlemn  34525  ballotlem2  34633  ballotlemodife  34642  oddprm2  34799  bnj257  34850  bnj268  34852  bnj290  34853  bnj312  34855  bnj89  34864  bnj887  34908  bnj976  34920  bnj1019  34922  bnj1146  34933  bnj1385  34974  bnj110  35000  bnj121  35012  bnj130  35016  bnj153  35022  bnj543  35035  bnj580  35055  bnj607  35058  bnj849  35067  bnj882  35068  bnj916  35075  bnj985v  35095  bnj985  35096  bnj1033  35111  bnj1083  35120  bnj1090  35121  bnj1128  35132  bnj1174  35145  bnj1228  35153  onvf1odlem1  35285  erdszelem1  35373  cvmliftlem15  35480  snmlval  35513  satfvsuclem2  35542  satfdm  35551  elmpst  35718  mpstrcl  35723  orbi2iALT  35867  untuni  35891  dfso3  35902  xpab  35908  dftr6  35933  coep  35934  coepr  35935  dffr5  35936  dfso2  35937  cnvco1  35941  cnvco2  35942  eldm3  35943  dfdm5  35955  dfrn5  35956  brsset  36069  idsset  36070  dfon3  36072  dfbigcup2  36079  dfom5b  36092  dffun10  36094  dfiota3  36103  fnimage  36109  brdomain  36113  brrange  36114  brimg  36117  brapply  36118  brcup  36119  brcap  36120  lemsuccf  36121  funpartlem  36124  brrestrict  36131  dfrecs2  36132  brub  36136  altopelaltxp  36158  rmoeqi  36369  rmoeqbii  36370  reueqi  36371  reueqbii  36372  sbceqbii  36373  disjeq1i  36374  cbvralvw2  36408  cbvrexvw2  36409  cbvrmovw2  36410  cbvreuvw2  36411  cbvsbcvw2  36412  cbvdisjvw2  36417  trer  36498  filnetlem4  36563  df3nandALT1  36581  imnand2  36584  mh-unprimbi  36726  bj-dfbi5  36839  bj-bixor  36856  bj-dfsbc  36946  bj-nnfnt  37047  bj-csbsnlem  37210  bj-rcleqf  37332  bj-sscon  37336  bj-pw0ALT  37356  bj-restpw  37404  bj-opelidb1  37467  bj-imdiridlem  37499  bj-imdirco  37504  wl-df3xor2  37785  wl-3xorrot  37793  wl-3xorcoma  37794  wl-3xornot  37797  wl-df2-3mintru2  37801  wl-df3-3mintru2  37802  wl-df4-3mintru2  37803  wl-equsalvw  37863  wl-sb9v  37874  iundif1  37915  poimirlem25  37966  poimirlem26  37967  poimirlem30  37971  ismblfin  37982  mbfposadd  37988  itg2addnclem2  37993  ftc1anc  38022  inixp  38049  prdstotbnd  38115  heibor1lem  38130  isrngohom  38286  isidl  38335  isfldidl2  38390  isdmn3  38395  sbccom2lem  38445  triantru3  38557  vvdifopab  38586  brres2  38594  eldmqsres  38614  inxpss  38638  ref5  38640  n0el2  38656  dfsucmap3  38784  trcoss2  38895  dfeqvrel2  38995  dfeqvrel3  38996  redundeq1  39034  redundpbi1  39036  refrelredund4  39040  funALTVfun  39104  dfeldisj3  39132  dfeldisj5  39134  pet0  39239  petid  39241  petidres  39243  petinidres  39245  petxrnidres  39247  mpet  39274  petincnvepres  39284  pet  39286  pmapglbx  40215  lhpexle3  40458  cdleme25cv  40804  dicelval3  41626  diclspsn  41640  lcfls1c  41982  sn-axrep5v  42658  sn-iotalem  42662  psspwb  42669  redvmptabs  42792  eu6w  43109  moxfr  43124  fphpd  43244  uniel  43645  dflim6  43692  onsucf1olem  43698  dflim7  43701  omge2  43726  oenassex  43746  safesnsupfilb  43845  ifpim1  43896  ifpnot  43897  ifpid2  43898  ifpim2  43899  ifpxorcor  43903  ifpnot23  43905  ifpananb  43933  ifpnannanb  43934  ifpxorxorb  43938  rp-fakeinunass  43942  snen1g  43951  pren2  43980  alephiso2  43985  undmrnresiss  44031  cnvssco  44033  cotrintab  44041  cnviun  44077  imaiun1  44078  coiun1  44079  elintima  44080  frege133d  44192  frege54cor0a  44290  or3or  44450  andi3or  44451  ntrneik4w  44527  k0004lem1  44574  ismnuprim  44721  ismnushort  44728  undisjrab  44733  nzss  44744  pm10.541  44794  compab  44868  onfrALTlem5  44969  onfrALTlem5VD  45311  rext0  45365  wfaxun  45426  brpermmodel  45430  permaxrep  45433  permaxpow  45436  permac8prim  45441  eluni2f  45533  euabsneu  47476  aiotaexb  47537  aiotavb  47538  r19.32  47546  3an4ancom24  47717  ichn  47916  ichcom  47919  ichbi12i  47920  prproropf1olem0  47962  pairreueq  47970  clnbgrsym  48314  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  sgrp2sgrp  48704  islindeps  48929  elbigo  49027  reutruALT  49280  coxp  49308  tposres0  49352  catcinv  49874  isthincd2  49912  setrec1lem3  50164  elpg  50189