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  2036  exexw  2051  sb3an  2081  sbcom4  2089  sbbiiev  2092  excom  2162  sbal  2169  19.32  2233  19.31  2234  19.42  2236  equsalv  2267  sbex  2281  sbrim  2304  sbor  2307  sbbi  2308  sbnfOLD  2313  cbvex2v  2345  eeeanv  2351  sbnf2  2360  cbvsbvf  2365  cbvex2  2416  equsal  2421  dfsb3  2498  mo4  2565  eu6  2573  eubii  2584  dfeu  2594  sb8eulem  2597  sb8mo  2600  cbvmovw  2601  cbvmow  2602  cbveuvw  2604  cbveuw  2605  cbveuALT  2607  eu1  2609  sbmo  2613  cbvabv  2805  cbvabw  2806  cbvab  2807  eqabcb  2876  nfceqi  2895  ralbii2  3078  rexbii2  3079  r19.26-3  3099  r19.43  3108  r2allem  3128  r19.21vOLD  3166  r19.42v  3176  r19.32v  3177  reeanlem  3212  3reeanv  3214  2ralorOLD  3216  cbvralvw  3220  cbvrexvw  3221  ralcom  3270  ralcomf  3282  rexcomf  3283  cbvralfw  3284  cbvralsvw  3296  cbvralf  3339  cbvrexf  3340  reu5  3361  rmobiia  3365  reubiia  3366  rmoanidOLD  3371  reuanidOLD  3372  rmo5  3379  cbvrmovw  3382  cbvreuvw  3383  moelOLD  3384  cbvrmow  3388  cbvreuw  3389  cbvreuwOLD  3394  cbvreu  3407  cbvrmo  3408  rabid2f  3447  rabid2OLD  3450  abv  3471  abvALT  3472  ceqsal  3498  ceqsalv  3500  cgsex4gOLD  3508  ceqsex3v  3516  ceqsex4v  3517  ceqsex8v  3519  reurab  3684  eueq  3691  reu2  3708  reu6  3709  reu3  3710  rmo4  3713  rmo3f  3717  2reu5  3741  cbvsbcw  3798  cbvsbcvw  3799  cbvsbc  3800  sbc3an  3830  sbccomlemOLD  3845  rmo3  3864  rmoanim  3869  rmoanimALT  3870  cbvralcsf  3916  cbvrexcsf  3917  cbvreucsf  3918  eqss  3974  uniiunlem  4062  sspsstri  4080  compleq  4127  ssequn1  4161  unss  4165  rexun  4171  ralunb  4172  elin3  4181  inass  4203  ssin  4214  elsymdif  4233  nssinpss  4242  dfun2  4245  difin  4247  indi  4259  indifdi  4269  difin2  4276  ssdif0  4341  inn0f  4346  inssdif0  4349  ab0  4355  abn0  4360  rabeq0w  4362  rabeq0  4363  disj  4425  disj3  4429  ssundif  4463  ralidmw  4483  dfif2  4502  eldifpr  4634  rexdifpr  4635  rexsns  4647  snprc  4693  reusn  4703  difsnpss  4783  tpss  4813  pwpr  4877  eluni2  4887  elunirab  4898  uniun  4906  unissb  4915  unissbOLD  4916  elintrab  4936  ssintrab  4947  intun  4956  iuncom  4975  iuncom4  4976  iunab  5027  ssiinf  5030  iunn0  5043  iinab  5044  iunin2  5047  iinun2  5049  iundif2  5050  iunun  5069  iunxun  5070  iunxiun  5073  sspwuni  5076  iinpw  5082  cbvdisj  5096  cbvdisjv  5097  disjor  5101  brun  5170  brin  5171  brdif  5172  dftr2  5231  dftr5  5233  intexrab  5317  inuni  5320  ssext  5429  pweqb  5431  otth2  5458  otthne  5461  propeqop  5482  vopelopabsb  5504  eqopab2bw  5523  eqopab2b  5527  pwin  5544  pwun  5546  dffr6  5609  elxp2  5678  otelxp  5698  xpiundi  5725  xpiundir  5726  poinxp  5735  soinxp  5736  frinxp  5737  seinxp  5738  weinxp  5739  inopab  5808  difopab  5809  difopabOLD  5810  inxp  5811  raliunxp  5819  rexiunxp  5820  rexxpf  5827  iunxpf  5828  cnvco  5865  dmiun  5893  dmuni  5894  dm0rn0  5904  dmres  5999  restidsing  6040  cnvsymOLDOLD  6103  asymref  6105  codir  6109  qfto  6110  cnvopab  6126  cnvopabOLD  6127  cnvdif  6132  rniun  6136  dminss  6142  imainss  6143  difxp  6153  xpdifid  6157  dmsnn0  6196  cnvcnvsn  6208  cnvresima  6219  resco  6239  imaco  6240  rnco  6241  coiun  6245  coass  6254  ressn  6274  cnviin  6275  cnvpo  6276  cnvso  6277  xpco  6278  opreu2reurex  6283  dfpo2  6285  imaindm  6288  dflim2  6410  funcnv  6604  funcnv3  6605  fncnv  6608  fun11  6609  imadif  6619  fnres  6664  dfmpt3  6671  mptfnf  6672  fnopabg  6674  fint  6756  fin  6757  fores  6799  dff1o3  6823  f1ompt  7100  fsn  7124  imaiun  7236  isocnv2  7323  isocnv3  7324  isores2  7325  isomin  7329  eqoprab2bw  7475  eqoprab2b  7476  elpwpwel  7759  sucexb  7796  onsucb  7809  dflim4  7841  fiun  7939  f1iun  7940  f11o  7943  opabex3d  7962  opabex3rd  7963  opabex3  7964  dfopab2  8049  dfoprab3s  8050  fmpox  8064  fparlem1  8109  fparlem2  8110  tpostpos  8243  frrlem9  8291  wfrlem8OLD  8328  wfrfunOLD  8331  dfsmo2  8359  brwitnlem  8517  oarec  8572  naddasslem1  8704  naddasslem2  8705  qsid  8795  uniinqs  8809  mapval2  8884  mapsncnv  8905  elixp2  8913  ixpin  8935  brsdom  8987  brdom2  8994  xpassen  9078  brsdom2  9109  dif1enOLD  9174  unfilem1  9313  fiint  9336  fiintOLD  9337  dfsup2  9454  supmo  9462  eqinf  9495  infmo  9507  brttrcl2  9726  rankc1  9882  cp  9903  isinfcard  10104  aceq1  10129  aceq2  10131  dfac5lem3  10137  dfac10b  10152  dfac12a  10161  dffin7-2  10410  dfacfin7  10411  fin1a2lem6  10417  iunfo  10551  konigthlem  10580  axgroth6  10840  axgroth3  10843  sstskm  10854  ltexprlem1  11048  gt0srpr  11090  ltpsrpr  11121  map2psrpr  11122  ltresr  11152  fimaxre3  12186  sup3  12197  supaddc  12207  supmul1  12209  elnn0z  12599  elznn0nn  12600  zmin  12958  xrnemnf  13131  xrnepnf  13132  dfrp2  13409  elioomnf  13459  elxrge0  13472  elfzuzb  13533  fzass4  13577  elfz2nn0  13633  elfzo2  13677  elfzo3  13691  lbfzo0  13714  fzo1lb  13728  fzind2  13799  nn0opthlem1  14284  hashgt23el  14440  cotr2g  14993  rexfiuz  15364  fsumcom2  15788  prodmo  15950  fprodcom2  15998  sinltx  16205  divalglem4  16413  divalglem10  16419  4sqlem12  16974  imasleval  17553  xpsfrnel  17574  xpscf  17577  isssc  17831  isffth2  17929  ispos2  18325  issubmgm  18678  ismhm  18761  issubmndb  18781  nsgacs  19143  isgim  19243  oppgcntz  19345  f1omvdco3  19428  pmtrprfvalrn  19467  efgrelexlemb  19729  pgpfac1  20061  pgpfac  20065  issrg  20146  opprsubg  20310  opprunit  20335  isirred2  20379  opprirred  20380  opprnzrb  20479  isdomn2OLD  20670  opprdomnb  20675  isdomn4r  20677  drngprop  20702  opprdrng  20722  issdrg2  20753  islss  20889  islbs  21032  unocv  21638  iunocv  21639  isbasis2g  22884  tgval2  22892  ntreq0  23013  isclo2  23024  cmpcov2  23326  is1stc2  23378  1stcelcls  23397  llyi  23410  unisngl  23463  txuni2  23501  xkobval  23522  hausdiag  23581  isfbas2  23771  elfg  23807  fbasrn  23820  fmfnfmlem3  23892  isfcls  23945  alexsubALTlem2  23984  istmd  24010  istgp  24013  istrg  24100  istdrg  24102  istdrg2  24114  isms2  24387  metuel2  24502  restmetu  24507  isngp  24533  isngp2  24534  isngp3  24535  elii1  24880  isncvsngp  25099  iscph  25120  isbn  25288  pmltpc  25401  ovolfcl  25417  finiunmbl  25495  iundisj  25499  dyaddisj  25547  vitalilem1  25559  ellimc3  25830  ig1pval3  26133  plyun0  26152  plydivex  26255  aannenlem2  26287  ellogrn  26518  atandm  26836  atandm3  26838  atans2  26891  elno3  27617  conway  27761  eqscut2  27768  madeval2  27809  tgjustf  28398  colinearalg  28835  axeuclid  28888  nbgrsym  29288  upgrtrls  29627  upgristrl  29628  dfpth2  29657  usgr2pth0  29693  iswwlks  29764  isclwwlk  29911  clwwlkneq0  29956  h2hlm  30907  issh  31135  chcon2i  31391  chcon1i  31392  chcon3i  31393  chnlei  31412  cmcm2i  31520  cmcm3i  31521  3oalem3  31591  pjdifnormii  31610  pjneli  31650  dfadj2  31812  cnvadj  31819  hhcno  31831  hhcnf  31832  eleigvec  31884  eleigvec2  31885  pjimai  32103  isst  32140  ishst  32141  cvnbtwn4  32216  chrelat4i  32300  2reucom  32407  reuxfrdf  32418  difrab2  32425  inpr0  32459  iunin1f  32484  disjnf  32497  cbvdisjf  32498  disjorf  32506  iundisjf  32516  disjexc  32520  xrdifh  32703  iundisjfi  32719  hashxpe  32732  pmtrprfv2  33045  xrnarchi  33128  isunit2  33181  isorng  33267  prmidl0  33411  opprnsg  33445  ccfldextdgrr  33659  cmpcref  33827  ordtconnlem1  33901  isrrext  33977  cntnevol  34205  ddemeas  34213  omssubaddlem  34277  omssubadd  34278  eulerpartleme  34341  eulerpartlemv  34342  eulerpartlemt0  34347  eulerpartlemgvv  34354  eulerpartlemn  34359  ballotlem2  34467  ballotlemodife  34476  oddprm2  34633  bnj257  34684  bnj268  34686  bnj290  34687  bnj312  34689  bnj89  34698  bnj887  34742  bnj976  34754  bnj1019  34756  bnj1146  34768  bnj1385  34809  bnj110  34835  bnj121  34847  bnj130  34851  bnj153  34857  bnj543  34870  bnj580  34890  bnj607  34893  bnj849  34902  bnj882  34903  bnj916  34910  bnj985v  34930  bnj985  34931  bnj1033  34946  bnj1083  34955  bnj1090  34956  bnj1128  34967  bnj1174  34980  bnj1228  34988  erdszelem1  35159  cvmliftlem15  35266  snmlval  35299  satfvsuclem2  35328  satfdm  35337  elmpst  35504  mpstrcl  35509  orbi2iALT  35653  untuni  35672  dfso3  35683  xpab  35689  dftr6  35714  coep  35715  coepr  35716  dffr5  35717  dfso2  35718  cnvco1  35722  cnvco2  35723  eldm3  35724  dfdm5  35736  dfrn5  35737  brsset  35853  idsset  35854  dfon3  35856  dfbigcup2  35863  dfom5b  35876  dffun10  35878  dfiota3  35887  fnimage  35893  brdomain  35897  brrange  35898  brimg  35901  brapply  35902  brcup  35903  brcap  35904  brsuccf  35905  funpartlem  35906  brrestrict  35913  dfrecs2  35914  brub  35918  altopelaltxp  35940  rmoeqi  36151  rmoeqbii  36152  reueqi  36153  reueqbii  36154  sbceqbii  36155  disjeq1i  36156  cbvralvw2  36190  cbvrexvw2  36191  cbvrmovw2  36192  cbvreuvw2  36193  cbvsbcvw2  36194  cbvdisjvw2  36199  trer  36280  filnetlem4  36345  df3nandALT1  36363  imnand2  36366  bj-dfbi5  36538  bj-bixor  36555  bj-nnfnt  36704  bj-csbsnlem  36867  bj-rcleqf  36989  bj-sscon  36993  bj-pw0ALT  37013  bj-restpw  37056  bj-opelidb1  37117  bj-imdiridlem  37149  bj-imdirco  37154  wl-df3xor2  37433  wl-3xorrot  37441  wl-3xorcoma  37442  wl-3xornot  37445  wl-df2-3mintru2  37449  wl-df3-3mintru2  37450  wl-df4-3mintru2  37451  wl-equsalvw  37502  wl-sb9v  37513  iundif1  37564  poimirlem25  37615  poimirlem26  37616  poimirlem30  37620  ismblfin  37631  mbfposadd  37637  itg2addnclem2  37642  ftc1anc  37671  inixp  37698  prdstotbnd  37764  heibor1lem  37779  isrngohom  37935  isidl  37984  isfldidl2  38039  isdmn3  38044  sbccom2lem  38094  triantru3  38194  vvdifopab  38224  brres2  38232  eldmqsres  38251  inxpss  38275  ref5  38277  n0el2  38297  trcoss2  38448  dfeqvrel2  38554  dfeqvrel3  38555  redundeq1  38593  redundpbi1  38595  refrelredund4  38599  funALTVfun  38662  dfeldisj3  38683  dfeldisj5  38685  pet0  38779  petid  38781  petidres  38783  petinidres  38785  petxrnidres  38787  mpet  38803  petincnvepres  38813  pet  38815  pmapglbx  39734  lhpexle3  39977  cdleme25cv  40323  dicelval3  41145  diclspsn  41159  lcfls1c  41501  sn-axrep5v  42213  sn-iotalem  42218  psspwb  42225  redvmptabs  42350  eu6w  42646  moxfr  42662  fphpd  42786  uniel  43188  dflim6  43235  onsucf1olem  43241  dflim7  43244  omge2  43269  oenassex  43289  safesnsupfilb  43389  ifpim1  43440  ifpnot  43441  ifpid2  43442  ifpim2  43443  ifpxorcor  43447  ifpnot23  43449  ifpananb  43477  ifpnannanb  43478  ifpxorxorb  43482  rp-fakeinunass  43486  snen1g  43495  pren2  43524  alephiso2  43529  undmrnresiss  43575  cnvssco  43577  cotrintab  43585  cnviun  43621  imaiun1  43622  coiun1  43623  elintima  43624  frege133d  43736  frege54cor0a  43834  or3or  43994  andi3or  43995  ntrneik4w  44071  k0004lem1  44118  ismnuprim  44266  ismnushort  44273  undisjrab  44278  nzss  44289  pm10.541  44339  compab  44414  onfrALTlem5  44515  onfrALTlem5VD  44857  rext0  44911  wfaxun  44972  brpermmodel  44976  permaxrep  44979  permaxpow  44982  eluni2f  45075  euabsneu  47005  aiotaexb  47066  aiotavb  47067  r19.32  47075  3an4ancom24  47246  ichn  47418  ichcom  47421  ichbi12i  47422  prproropf1olem0  47464  pairreueq  47472  clnbgrsym  47799  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  sgrp2sgrp  48151  islindeps  48377  elbigo  48479  reutruALT  48732  coxp  48759  tposres0  48800  isthincd2  49271  setrec1lem3  49501  elpg  49526