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  648  pm4.14  806  or4  926  orimdi  930  orbidi  954  ordi  1007  ordir  1008  andir  1010  dfbi3  1049  dfifp7  1069  ifpdfbi  1070  ifpn  1073  3orrot  1091  3orcoma  1092  3ioran  1105  3ianor  1106  3anbi123i  1155  3orbi123i  1156  3jaob  1428  an6  1447  3or6  1449  an3andi  1484  an33rean  1485  nancom  1496  xorass  1515  anxordi  1526  norass  1537  hadbi  1598  hadcoma  1599  hadcomb  1600  hadnot  1602  cador  1608  cadan  1609  cadcoma  1612  cadnot  1615  nic-axALT  1674  19.26-3an  1872  19.43OLD  1883  19.32v  1940  19.31v  1941  19.42v  1953  4exdistr  1961  cbvexvw  2037  exexw  2052  sb3an  2082  sbcom4  2090  sbbiiev  2093  excom  2163  sbal  2170  19.32  2234  19.31  2235  19.42  2237  equsalv  2268  sbex  2281  sbrim  2304  sbor  2306  sbbi  2307  sbnfOLD  2312  cbvex2v  2342  eeeanv  2348  sbnf2  2357  cbvsbvf  2362  cbvex2  2411  equsal  2416  dfsb3  2493  mo4  2560  eu6  2568  eubii  2579  dfeu  2589  sb8eulem  2592  sb8mo  2595  cbvmovw  2596  cbvmow  2597  cbveuvw  2599  cbveuw  2600  cbveuALT  2602  eu1  2604  sbmo  2608  cbvabv  2800  cbvabw  2801  cbvab  2802  eqabcb  2870  nfceqi  2889  ralbii2  3072  rexbii2  3073  r19.26-3  3093  r19.43  3102  r2allem  3122  r19.21vOLD  3160  r19.42v  3170  r19.32v  3171  reeanlem  3209  3reeanv  3211  cbvralvw  3216  cbvrexvw  3217  ralcom  3266  ralcomf  3278  rexcomf  3279  cbvralfw  3280  cbvralsvw  3292  cbvralf  3336  cbvrexf  3337  reu5  3358  rmobiia  3362  reubiia  3363  rmoanidOLD  3368  reuanidOLD  3369  rmo5  3376  cbvrmovw  3379  cbvreuvw  3380  cbvrmow  3383  cbvreuw  3384  cbvreuwOLD  3389  cbvreu  3400  cbvrmo  3401  rabid2f  3440  abv  3462  abvALT  3463  ceqsal  3488  ceqsalv  3490  cgsex4gOLD  3498  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  reurab  3675  eueq  3682  reu2  3699  reu6  3700  reu3  3701  rmo4  3704  rmo3f  3708  2reu5  3732  cbvsbcw  3789  cbvsbcvw  3790  cbvsbc  3791  sbc3an  3821  sbccomlemOLD  3836  rmo3  3855  rmoanim  3860  rmoanimALT  3861  cbvralcsf  3907  cbvrexcsf  3908  cbvreucsf  3909  eqss  3965  uniiunlem  4053  sspsstri  4071  compleq  4118  ssequn1  4152  unss  4156  rexun  4162  ralunb  4163  elin3  4172  inass  4194  ssin  4205  elsymdif  4224  nssinpss  4233  dfun2  4236  difin  4238  indi  4250  indifdi  4260  difin2  4267  ssdif0  4332  inn0f  4337  inssdif0  4340  ab0  4346  abn0  4351  rabeq0w  4353  rabeq0  4354  disj  4416  disj3  4420  ssundif  4454  ralidmw  4474  dfif2  4493  eldifpr  4625  rexdifpr  4626  rexsns  4638  snprc  4684  reusn  4694  difsnpss  4774  tpss  4804  pwpr  4868  eluni2  4878  elunirab  4889  uniun  4897  unissb  4906  unissbOLD  4907  elintrab  4927  ssintrab  4938  intun  4947  iuncom  4966  iuncom4  4967  iunab  5018  ssiinf  5021  iunn0  5034  iinab  5035  iunin2  5038  iinun2  5040  iundif2  5041  iunun  5060  iunxun  5061  iunxiun  5064  sspwuni  5067  iinpw  5073  cbvdisj  5087  cbvdisjv  5088  disjor  5092  brun  5161  brin  5162  brdif  5163  dftr2  5219  dftr5  5221  intexrab  5305  inuni  5308  ssext  5417  pweqb  5419  otth2  5446  otthne  5449  propeqop  5470  vopelopabsb  5492  eqopab2bw  5511  eqopab2b  5515  pwin  5532  pwun  5534  dffr6  5597  elxp2  5665  otelxp  5685  xpiundi  5712  xpiundir  5713  poinxp  5722  soinxp  5723  frinxp  5724  seinxp  5725  weinxp  5726  inopab  5795  difopab  5796  difopabOLD  5797  inxp  5798  raliunxp  5806  rexiunxp  5807  rexxpf  5814  iunxpf  5815  cnvco  5852  dmiun  5880  dmuni  5881  dm0rn0  5891  dmres  5986  restidsing  6027  cnvsymOLDOLD  6090  asymref  6092  codir  6096  qfto  6097  cnvopab  6113  cnvopabOLD  6114  cnvdif  6119  rniun  6123  dminss  6129  imainss  6130  difxp  6140  xpdifid  6144  dmsnn0  6183  cnvcnvsn  6195  cnvresima  6206  resco  6226  imaco  6227  rnco  6228  coiun  6232  coass  6241  ressn  6261  cnviin  6262  cnvpo  6263  cnvso  6264  xpco  6265  opreu2reurex  6270  dfpo2  6272  imaindm  6275  dflim2  6393  funcnv  6588  funcnv3  6589  fncnv  6592  fun11  6593  imadif  6603  fnres  6648  dfmpt3  6655  mptfnf  6656  fnopabg  6658  fint  6742  fin  6743  fores  6785  dff1o3  6809  f1ompt  7086  fsn  7110  imaiun  7222  isocnv2  7309  isocnv3  7310  isores2  7311  isomin  7315  eqoprab2bw  7462  eqoprab2b  7463  elpwpwel  7746  sucexb  7783  onsucb  7795  dflim4  7827  fiun  7924  f1iun  7925  f11o  7928  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfopab2  8034  dfoprab3s  8035  fmpox  8049  fparlem1  8094  fparlem2  8095  tpostpos  8228  frrlem9  8276  dfsmo2  8319  brwitnlem  8474  oarec  8529  naddasslem1  8661  naddasslem2  8662  qsid  8757  uniinqs  8773  mapval2  8848  mapsncnv  8869  elixp2  8877  ixpin  8899  brsdom  8949  brdom2  8956  xpassen  9040  brsdom2  9071  dif1enOLD  9132  unfilem1  9261  fiint  9284  fiintOLD  9285  dfsup2  9402  supmo  9410  eqinf  9443  infmo  9455  brttrcl2  9674  rankc1  9830  cp  9851  isinfcard  10052  aceq1  10077  aceq2  10079  dfac5lem3  10085  dfac10b  10100  dfac12a  10109  dffin7-2  10358  dfacfin7  10359  fin1a2lem6  10365  iunfo  10499  konigthlem  10528  axgroth6  10788  axgroth3  10791  sstskm  10802  ltexprlem1  10996  gt0srpr  11038  ltpsrpr  11069  map2psrpr  11070  ltresr  11100  fimaxre3  12136  sup3  12147  supaddc  12157  supmul1  12159  elnn0z  12549  elznn0nn  12550  zmin  12910  xrnemnf  13084  xrnepnf  13085  dfrp2  13362  elioomnf  13412  elxrge0  13425  elfzuzb  13486  fzass4  13530  elfz2nn0  13586  elfzo2  13630  elfzo3  13644  lbfzo0  13667  fzo1lb  13681  fzind2  13753  nn0opthlem1  14240  hashgt23el  14396  cotr2g  14949  rexfiuz  15321  fsumcom2  15747  prodmo  15909  fprodcom2  15957  sinltx  16164  divalglem4  16373  divalglem10  16379  4sqlem12  16934  imasleval  17511  xpsfrnel  17532  xpscf  17535  isssc  17789  isffth2  17887  ispos2  18283  issubmgm  18636  ismhm  18719  issubmndb  18739  nsgacs  19101  isgim  19201  oppgcntz  19303  f1omvdco3  19386  pmtrprfvalrn  19425  efgrelexlemb  19687  pgpfac1  20019  pgpfac  20023  issrg  20104  opprsubg  20268  opprunit  20293  isirred2  20337  opprirred  20338  opprnzrb  20437  isdomn2OLD  20628  opprdomnb  20633  isdomn4r  20635  drngprop  20660  opprdrng  20680  issdrg2  20711  islss  20847  islbs  20990  unocv  21596  iunocv  21597  isbasis2g  22842  tgval2  22850  ntreq0  22971  isclo2  22982  cmpcov2  23284  is1stc2  23336  1stcelcls  23355  llyi  23368  unisngl  23421  txuni2  23459  xkobval  23480  hausdiag  23539  isfbas2  23729  elfg  23765  fbasrn  23778  fmfnfmlem3  23850  isfcls  23903  alexsubALTlem2  23942  istmd  23968  istgp  23971  istrg  24058  istdrg  24060  istdrg2  24072  isms2  24345  metuel2  24460  restmetu  24465  isngp  24491  isngp2  24492  isngp3  24493  elii1  24838  isncvsngp  25056  iscph  25077  isbn  25245  pmltpc  25358  ovolfcl  25374  finiunmbl  25452  iundisj  25456  dyaddisj  25504  vitalilem1  25516  ellimc3  25787  ig1pval3  26090  plyun0  26109  plydivex  26212  aannenlem2  26244  ellogrn  26475  atandm  26793  atandm3  26795  atans2  26848  elno3  27574  conway  27718  eqscut2  27725  madeval2  27768  tgjustf  28407  colinearalg  28844  axeuclid  28897  nbgrsym  29297  upgrtrls  29636  upgristrl  29637  dfpth2  29666  usgr2pth0  29702  iswwlks  29773  isclwwlk  29920  clwwlkneq0  29965  h2hlm  30916  issh  31144  chcon2i  31400  chcon1i  31401  chcon3i  31402  chnlei  31421  cmcm2i  31529  cmcm3i  31530  3oalem3  31600  pjdifnormii  31619  pjneli  31659  dfadj2  31821  cnvadj  31828  hhcno  31840  hhcnf  31841  eleigvec  31893  eleigvec2  31894  pjimai  32112  isst  32149  ishst  32150  cvnbtwn4  32225  chrelat4i  32309  2reucom  32416  reuxfrdf  32427  difrab2  32434  inpr0  32468  iunin1f  32493  disjnf  32506  cbvdisjf  32507  disjorf  32515  iundisjf  32525  disjexc  32529  xrdifh  32710  iundisjfi  32726  hashxpe  32739  pmtrprfv2  33052  xrnarchi  33145  isunit2  33198  isorng  33284  prmidl0  33428  opprnsg  33462  ccfldextdgrr  33674  cmpcref  33847  ordtconnlem1  33921  isrrext  33997  cntnevol  34225  ddemeas  34233  omssubaddlem  34297  omssubadd  34298  eulerpartleme  34361  eulerpartlemv  34362  eulerpartlemt0  34367  eulerpartlemgvv  34374  eulerpartlemn  34379  ballotlem2  34487  ballotlemodife  34496  oddprm2  34653  bnj257  34704  bnj268  34706  bnj290  34707  bnj312  34709  bnj89  34718  bnj887  34762  bnj976  34774  bnj1019  34776  bnj1146  34788  bnj1385  34829  bnj110  34855  bnj121  34867  bnj130  34871  bnj153  34877  bnj543  34890  bnj580  34910  bnj607  34913  bnj849  34922  bnj882  34923  bnj916  34930  bnj985v  34950  bnj985  34951  bnj1033  34966  bnj1083  34975  bnj1090  34976  bnj1128  34987  bnj1174  35000  bnj1228  35008  onvf1odlem1  35097  erdszelem1  35185  cvmliftlem15  35292  snmlval  35325  satfvsuclem2  35354  satfdm  35363  elmpst  35530  mpstrcl  35535  orbi2iALT  35679  untuni  35703  dfso3  35714  xpab  35720  dftr6  35745  coep  35746  coepr  35747  dffr5  35748  dfso2  35749  cnvco1  35753  cnvco2  35754  eldm3  35755  dfdm5  35767  dfrn5  35768  brsset  35884  idsset  35885  dfon3  35887  dfbigcup2  35894  dfom5b  35907  dffun10  35909  dfiota3  35918  fnimage  35924  brdomain  35928  brrange  35929  brimg  35932  brapply  35933  brcup  35934  brcap  35935  brsuccf  35936  funpartlem  35937  brrestrict  35944  dfrecs2  35945  brub  35949  altopelaltxp  35971  rmoeqi  36182  rmoeqbii  36183  reueqi  36184  reueqbii  36185  sbceqbii  36186  disjeq1i  36187  cbvralvw2  36221  cbvrexvw2  36222  cbvrmovw2  36223  cbvreuvw2  36224  cbvsbcvw2  36225  cbvdisjvw2  36230  trer  36311  filnetlem4  36376  df3nandALT1  36394  imnand2  36397  bj-dfbi5  36569  bj-bixor  36586  bj-nnfnt  36735  bj-csbsnlem  36898  bj-rcleqf  37020  bj-sscon  37024  bj-pw0ALT  37044  bj-restpw  37087  bj-opelidb1  37148  bj-imdiridlem  37180  bj-imdirco  37185  wl-df3xor2  37464  wl-3xorrot  37472  wl-3xorcoma  37473  wl-3xornot  37476  wl-df2-3mintru2  37480  wl-df3-3mintru2  37481  wl-df4-3mintru2  37482  wl-equsalvw  37533  wl-sb9v  37544  iundif1  37595  poimirlem25  37646  poimirlem26  37647  poimirlem30  37651  ismblfin  37662  mbfposadd  37668  itg2addnclem2  37673  ftc1anc  37702  inixp  37729  prdstotbnd  37795  heibor1lem  37810  isrngohom  37966  isidl  38015  isfldidl2  38070  isdmn3  38075  sbccom2lem  38125  triantru3  38225  vvdifopab  38256  brres2  38264  eldmqsres  38282  inxpss  38306  ref5  38308  n0el2  38324  trcoss2  38482  dfeqvrel2  38588  dfeqvrel3  38589  redundeq1  38627  redundpbi1  38629  refrelredund4  38633  funALTVfun  38697  dfeldisj3  38718  dfeldisj5  38720  pet0  38814  petid  38816  petidres  38818  petinidres  38820  petxrnidres  38822  mpet  38838  petincnvepres  38848  pet  38850  pmapglbx  39770  lhpexle3  40013  cdleme25cv  40359  dicelval3  41181  diclspsn  41195  lcfls1c  41537  sn-axrep5v  42211  sn-iotalem  42216  psspwb  42223  redvmptabs  42355  eu6w  42671  moxfr  42687  fphpd  42811  uniel  43213  dflim6  43260  onsucf1olem  43266  dflim7  43269  omge2  43294  oenassex  43314  safesnsupfilb  43414  ifpim1  43465  ifpnot  43466  ifpid2  43467  ifpim2  43468  ifpxorcor  43472  ifpnot23  43474  ifpananb  43502  ifpnannanb  43503  ifpxorxorb  43507  rp-fakeinunass  43511  snen1g  43520  pren2  43549  alephiso2  43554  undmrnresiss  43600  cnvssco  43602  cotrintab  43610  cnviun  43646  imaiun1  43647  coiun1  43648  elintima  43649  frege133d  43761  frege54cor0a  43859  or3or  44019  andi3or  44020  ntrneik4w  44096  k0004lem1  44143  ismnuprim  44290  ismnushort  44297  undisjrab  44302  nzss  44313  pm10.541  44363  compab  44438  onfrALTlem5  44539  onfrALTlem5VD  44881  rext0  44935  wfaxun  44996  brpermmodel  45000  permaxrep  45003  permaxpow  45006  permac8prim  45011  eluni2f  45104  euabsneu  47033  aiotaexb  47094  aiotavb  47095  r19.32  47103  3an4ancom24  47274  ichn  47461  ichcom  47464  ichbi12i  47465  prproropf1olem0  47507  pairreueq  47515  clnbgrsym  47842  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  sgrp2sgrp  48220  islindeps  48446  elbigo  48544  reutruALT  48797  coxp  48825  tposres0  48869  catcinv  49392  isthincd2  49430  setrec1lem3  49682  elpg  49707