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  1497  xorass  1516  anxordi  1527  norass  1538  hadbi  1599  hadcoma  1600  hadcomb  1601  hadnot  1603  cador  1609  cadan  1610  cadcoma  1613  cadnot  1616  nic-axALT  1675  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1962  cbvexvw  2038  exexw  2054  sb3an  2086  sbcom4  2094  sbbiiev  2097  excom  2167  sbal  2174  19.32  2238  19.31  2239  19.42  2241  equsalv  2272  sbex  2285  sbrim  2308  sbor  2310  sbbi  2311  sbnfOLD  2316  cbvex2v  2346  eeeanv  2352  sbnf2  2360  cbvsbvf  2365  cbvex2  2414  equsal  2419  dfsb3  2496  mo4  2563  eu6  2571  eubii  2582  dfeu  2592  sb8eulem  2595  sb8mo  2598  cbvmovw  2599  cbvmow  2600  cbveuvw  2602  cbveuw  2603  cbveuALT  2605  eu1  2607  sbmo  2611  cbvabv  2803  cbvabw  2804  cbvab  2805  eqabcbw  2807  eqabcb  2873  nfceqi  2892  ralbii2  3075  rexbii2  3076  r19.26-3  3094  r19.43  3101  r2allem  3121  r19.42v  3165  r19.32v  3166  reeanlem  3204  3reeanv  3206  cbvralvw  3211  cbvrexvw  3212  ralcom  3261  ralcomf  3271  rexcomf  3272  cbvralfw  3273  cbvralsvw  3284  cbvralf  3327  cbvrexf  3328  reu5  3349  rmobiia  3353  reubiia  3354  rmo5  3365  cbvrmovw  3368  cbvreuvw  3369  cbvrmow  3372  cbvreuw  3373  cbvreu  3388  cbvrmo  3389  rabid2f  3427  abv  3449  abvALT  3450  ceqsal  3475  ceqsalv  3477  cgsex4gOLD  3485  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  reurab  3656  eueq  3663  reu2  3680  reu6  3681  reu3  3682  rmo4  3685  rmo3f  3689  2reu5  3713  cbvsbcw  3770  cbvsbcvw  3771  cbvsbc  3772  sbc3an  3802  sbccomlemOLD  3817  rmo3  3836  rmoanim  3841  rmoanimALT  3842  cbvralcsf  3888  cbvrexcsf  3889  cbvreucsf  3890  eqss  3946  uniiunlem  4036  sspsstri  4054  compleq  4101  ssequn1  4135  unss  4139  rexun  4145  ralunb  4146  elin3  4155  inass  4177  ssin  4188  elsymdif  4207  nssinpss  4216  dfun2  4219  difin  4221  indi  4233  indifdi  4243  difin2  4250  eq0  4299  ssdif0  4315  inn0f  4320  inssdif0  4323  ab0w  4328  ab0  4329  ab0orv  4332  abn0  4334  rabeq0w  4336  rabeq0  4337  disj3  4403  ssundif  4437  ralidmw  4466  dfif2  4478  eldifpr  4612  rexdifpr  4613  rexsns  4625  snprc  4671  reusn  4681  difsnpss  4760  tpss  4790  pwpr  4854  eluni2  4864  elunirab  4875  uniun  4883  unissb  4893  elintrab  4912  ssintrab  4923  intun  4932  iuncom  4951  iuncom4  4952  iunab  5004  ssiinf  5007  iunn0  5019  iinab  5020  iunin2  5023  iinun2  5025  iundif2  5026  iunun  5045  iunxun  5046  iunxiun  5049  sspwuni  5052  iinpw  5058  cbvdisj  5072  cbvdisjv  5073  disjor  5077  brun  5146  brin  5147  brdif  5148  dftr2  5204  dftr5  5206  intexrab  5289  inuni  5292  ssext  5399  pweqb  5401  otth2  5428  otthne  5431  propeqop  5452  vopelopabsb  5474  eqopab2bw  5493  eqopab2b  5497  pwin  5512  pwun  5514  dffr6  5577  elxp2  5645  otelxp  5665  xpiundi  5692  xpiundir  5693  poinxp  5702  soinxp  5703  frinxp  5704  seinxp  5705  weinxp  5706  reliun  5762  inopab  5775  difopab  5776  inxp  5777  raliunxp  5785  rexiunxp  5786  rexxpf  5793  iunxpf  5794  cnvco  5831  dmiun  5859  dmuni  5860  dm0rn0  5870  dm0rn0OLD  5871  dmres  5968  restidsing  6009  asymref  6070  codir  6074  qfto  6075  cnvopab  6091  cnvopabOLD  6092  cnvdif  6098  rniun  6102  dminss  6108  imainss  6109  difxp  6119  xpdifid  6123  dmsnn0  6162  cnvcnvsn  6174  cnvresima  6185  resco  6205  imaco  6206  rnco  6207  rncoOLD  6208  coiun  6212  coass  6221  ressn  6240  cnviin  6241  cnvpo  6242  cnvso  6243  xpco  6244  opreu2reurex  6249  dfpo2  6251  imaindm  6254  dflim2  6372  funcnv  6558  funcnv3  6559  fncnv  6562  fun11  6563  imadif  6573  fnres  6616  dfmpt3  6623  mptfnf  6624  fnopabg  6626  fint  6710  fin  6711  fores  6753  dff1o3  6777  f1ompt  7053  fsn  7077  imaiun  7188  isocnv2  7274  isocnv3  7275  isores2  7276  isomin  7280  eqoprab2bw  7425  eqoprab2b  7426  elpwpwel  7709  sucexb  7746  onsucb  7756  dflim4  7787  fiun  7884  f1iun  7885  f11o  7888  opabex3d  7906  opabex3rd  7907  opabex3  7908  dfopab2  7993  dfoprab3s  7994  fmpox  8008  fparlem1  8051  fparlem2  8052  tpostpos  8185  frrlem9  8233  dfsmo2  8276  brwitnlem  8431  oarec  8486  naddasslem1  8618  naddasslem2  8619  qsid  8714  uniinqs  8730  mapval2  8806  mapsncnv  8827  elixp2  8835  ixpin  8857  brsdom  8907  brdom2  8915  xpassen  8995  brsdom2  9025  unfilem1  9200  fiint  9222  dfsup2  9339  supmo  9347  eqinf  9380  infmo  9392  brttrcl2  9615  rankc1  9774  cp  9795  isinfcard  9994  aceq1  10019  aceq2  10021  dfac5lem3  10027  dfac10b  10042  dfac12a  10051  dffin7-2  10300  dfacfin7  10301  fin1a2lem6  10307  iunfo  10441  konigthlem  10470  axgroth6  10730  axgroth3  10733  sstskm  10744  ltexprlem1  10938  gt0srpr  10980  ltpsrpr  11011  map2psrpr  11012  ltresr  11042  fimaxre3  12079  sup3  12090  supaddc  12100  supmul1  12102  elnn0z  12492  elznn0nn  12493  zmin  12848  xrnemnf  13022  xrnepnf  13023  dfrp2  13301  elioomnf  13351  elxrge0  13364  elfzuzb  13425  fzass4  13469  elfz2nn0  13525  elfzo2  13569  elfzo3  13583  lbfzo0  13606  fzo1lb  13620  fzind2  13695  nn0opthlem1  14182  hashgt23el  14338  cotr2g  14890  rexfiuz  15262  fsumcom2  15688  prodmo  15850  fprodcom2  15898  sinltx  16105  divalglem4  16314  divalglem10  16320  4sqlem12  16875  imasleval  17453  xpsfrnel  17474  xpscf  17477  isssc  17735  isffth2  17833  ispos2  18229  issubmgm  18618  ismhm  18701  issubmndb  18721  nsgacs  19082  isgim  19182  oppgcntz  19284  f1omvdco3  19369  pmtrprfvalrn  19408  efgrelexlemb  19670  pgpfac1  20002  pgpfac  20006  issrg  20114  opprsubg  20279  opprunit  20304  isirred2  20348  opprirred  20349  opprnzrb  20445  isdomn2OLD  20636  opprdomnb  20641  isdomn4r  20643  drngprop  20668  opprdrng  20688  issdrg2  20719  isorng  20785  islss  20876  islbs  21019  unocv  21626  iunocv  21627  isbasis2g  22883  tgval2  22891  ntreq0  23012  isclo2  23023  cmpcov2  23325  is1stc2  23377  1stcelcls  23396  llyi  23409  unisngl  23462  txuni2  23500  xkobval  23521  hausdiag  23580  isfbas2  23770  elfg  23806  fbasrn  23819  fmfnfmlem3  23891  isfcls  23944  alexsubALTlem2  23983  istmd  24009  istgp  24012  istrg  24099  istdrg  24101  istdrg2  24113  isms2  24385  metuel2  24500  restmetu  24505  isngp  24531  isngp2  24532  isngp3  24533  elii1  24878  isncvsngp  25096  iscph  25117  isbn  25285  pmltpc  25398  ovolfcl  25414  finiunmbl  25492  iundisj  25496  dyaddisj  25544  vitalilem1  25556  ellimc3  25827  ig1pval3  26130  plyun0  26149  plydivex  26252  aannenlem2  26284  ellogrn  26515  atandm  26833  atandm3  26835  atans2  26888  elno3  27614  conway  27760  eqscut2  27767  madeval2  27814  tgjustf  28471  colinearalg  28909  axeuclid  28962  nbgrsym  29362  upgrtrls  29699  upgristrl  29700  dfpth2  29728  usgr2pth0  29764  iswwlks  29835  isclwwlk  29985  clwwlkneq0  30030  h2hlm  30981  issh  31209  chcon2i  31465  chcon1i  31466  chcon3i  31467  chnlei  31486  cmcm2i  31594  cmcm3i  31595  3oalem3  31665  pjdifnormii  31684  pjneli  31724  dfadj2  31886  cnvadj  31893  hhcno  31905  hhcnf  31906  eleigvec  31958  eleigvec2  31959  pjimai  32177  isst  32214  ishst  32215  cvnbtwn4  32290  chrelat4i  32374  2reucom  32480  reuxfrdf  32491  difrab2  32498  inpr0  32533  iunin1f  32558  disjnf  32571  cbvdisjf  32572  disjorf  32580  iundisjf  32590  disjexc  32594  xrdifh  32788  iundisjfi  32804  hashxpe  32815  pmtrprfv2  33098  xrnarchi  33194  isunit2  33250  prmidl0  33459  opprnsg  33493  ccfldextdgrr  33757  cmpcref  33935  ordtconnlem1  34009  isrrext  34085  cntnevol  34313  ddemeas  34321  omssubaddlem  34384  omssubadd  34385  eulerpartleme  34448  eulerpartlemv  34449  eulerpartlemt0  34454  eulerpartlemgvv  34461  eulerpartlemn  34466  ballotlem2  34574  ballotlemodife  34583  oddprm2  34740  bnj257  34791  bnj268  34793  bnj290  34794  bnj312  34796  bnj89  34805  bnj887  34849  bnj976  34861  bnj1019  34863  bnj1146  34875  bnj1385  34916  bnj110  34942  bnj121  34954  bnj130  34958  bnj153  34964  bnj543  34977  bnj580  34997  bnj607  35000  bnj849  35009  bnj882  35010  bnj916  35017  bnj985v  35037  bnj985  35038  bnj1033  35053  bnj1083  35062  bnj1090  35063  bnj1128  35074  bnj1174  35087  bnj1228  35095  onvf1odlem1  35219  erdszelem1  35307  cvmliftlem15  35414  snmlval  35447  satfvsuclem2  35476  satfdm  35485  elmpst  35652  mpstrcl  35657  orbi2iALT  35801  untuni  35825  dfso3  35836  xpab  35842  dftr6  35867  coep  35868  coepr  35869  dffr5  35870  dfso2  35871  cnvco1  35875  cnvco2  35876  eldm3  35877  dfdm5  35889  dfrn5  35890  brsset  36003  idsset  36004  dfon3  36006  dfbigcup2  36013  dfom5b  36026  dffun10  36028  dfiota3  36037  fnimage  36043  brdomain  36047  brrange  36048  brimg  36051  brapply  36052  brcup  36053  brcap  36054  lemsuccf  36055  funpartlem  36058  brrestrict  36065  dfrecs2  36066  brub  36070  altopelaltxp  36092  rmoeqi  36303  rmoeqbii  36304  reueqi  36305  reueqbii  36306  sbceqbii  36307  disjeq1i  36308  cbvralvw2  36342  cbvrexvw2  36343  cbvrmovw2  36344  cbvreuvw2  36345  cbvsbcvw2  36346  cbvdisjvw2  36351  trer  36432  filnetlem4  36497  df3nandALT1  36515  imnand2  36518  bj-dfbi5  36690  bj-bixor  36707  bj-nnfnt  36857  bj-csbsnlem  37020  bj-rcleqf  37142  bj-sscon  37146  bj-pw0ALT  37166  bj-restpw  37209  bj-opelidb1  37270  bj-imdiridlem  37302  bj-imdirco  37307  wl-df3xor2  37586  wl-3xorrot  37594  wl-3xorcoma  37595  wl-3xornot  37598  wl-df2-3mintru2  37602  wl-df3-3mintru2  37603  wl-df4-3mintru2  37604  wl-equsalvw  37655  wl-sb9v  37666  iundif1  37707  poimirlem25  37758  poimirlem26  37759  poimirlem30  37763  ismblfin  37774  mbfposadd  37780  itg2addnclem2  37785  ftc1anc  37814  inixp  37841  prdstotbnd  37907  heibor1lem  37922  isrngohom  38078  isidl  38127  isfldidl2  38182  isdmn3  38187  sbccom2lem  38237  triantru3  38344  vvdifopab  38370  brres2  38378  eldmqsres  38398  inxpss  38422  ref5  38424  n0el2  38440  dfsucmap3  38549  trcoss2  38659  dfeqvrel2  38759  dfeqvrel3  38760  redundeq1  38798  redundpbi1  38800  refrelredund4  38804  funALTVfun  38869  dfeldisj3  38890  dfeldisj5  38892  pet0  38986  petid  38988  petidres  38990  petinidres  38992  petxrnidres  38994  mpet  39010  petincnvepres  39020  pet  39022  pmapglbx  39941  lhpexle3  40184  cdleme25cv  40530  dicelval3  41352  diclspsn  41366  lcfls1c  41708  sn-axrep5v  42387  sn-iotalem  42392  psspwb  42399  redvmptabs  42530  eu6w  42834  moxfr  42849  fphpd  42973  uniel  43374  dflim6  43421  onsucf1olem  43427  dflim7  43430  omge2  43455  oenassex  43475  safesnsupfilb  43575  ifpim1  43626  ifpnot  43627  ifpid2  43628  ifpim2  43629  ifpxorcor  43633  ifpnot23  43635  ifpananb  43663  ifpnannanb  43664  ifpxorxorb  43668  rp-fakeinunass  43672  snen1g  43681  pren2  43710  alephiso2  43715  undmrnresiss  43761  cnvssco  43763  cotrintab  43771  cnviun  43807  imaiun1  43808  coiun1  43809  elintima  43810  frege133d  43922  frege54cor0a  44020  or3or  44180  andi3or  44181  ntrneik4w  44257  k0004lem1  44304  ismnuprim  44451  ismnushort  44458  undisjrab  44463  nzss  44474  pm10.541  44524  compab  44598  onfrALTlem5  44699  onfrALTlem5VD  45041  rext0  45095  wfaxun  45156  brpermmodel  45160  permaxrep  45163  permaxpow  45166  permac8prim  45171  eluni2f  45263  euabsneu  47190  aiotaexb  47251  aiotavb  47252  r19.32  47260  3an4ancom24  47431  ichn  47618  ichcom  47621  ichbi12i  47622  prproropf1olem0  47664  pairreueq  47672  clnbgrsym  48000  usgrexmpl2nb0  48193  usgrexmpl2nb1  48194  usgrexmpl2nb2  48195  usgrexmpl2nb3  48196  usgrexmpl2nb4  48197  usgrexmpl2nb5  48198  sgrp2sgrp  48390  islindeps  48615  elbigo  48713  reutruALT  48966  coxp  48994  tposres0  49038  catcinv  49560  isthincd2  49598  setrec1lem3  49850  elpg  49875