Theorem 3bitr4i 306

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi2d  345  pm4.71  567  pm5.32ri  586  an31  661  pm4.14  819  or4  940  orimdi  944  orbidi  967  ordi  1023  ordir  1024  andir  1026  dfbi3  1065  dfifp7  1085  ifpdfbiOLD  1087  ifpn  1090  3orrot  1108  3orcoma  1109  3ioran  1123  3ianor  1124  3anbi123i  1173  3orbi123i  1174  3jaob  1453  an6  1474  3or6  1476  an3andi  1513  an33rean  1514  nancom  1526  xorass  1545  anxordi  1556  norass  1567  hadbi  1628  hadcoma  1629  hadcomb  1630  hadnot  1632  cador  1641  cadan  1642  cadcoma  1645  cadnot  1648  nic-axALT  1707  19.26-3an  1905  19.43OLD  1916  19.32v  1973  19.31v  1974  19.42v  1986  4exdistr  1994  cbvexvw  2070  exexw  2086  sb3an  2118  sbcom4  2126  sbbiiev  2130  excom  2199  sbal  2206  19.32  2269  19.31  2270  19.42  2272  equsalv  2301  sbex  2314  sbrim  2337  sbor  2339  sbbi  2340  cbvex2v  2373  eeeanv  2379  sbnf2  2387  cbvsbvf  2392  cbvex2  2441  equsal  2446  dfsb3  2523  mo4  2591  eu6  2599  dfeu  2620  sb8eulem  2623  sb8mo  2626  cbvmovw  2627  cbvmow  2628  cbveuvw  2630  cbveuw  2631  cbveuALT  2633  eu1  2635  sbmo  2639  cbvabv  2830  cbvabw  2831  cbvab  2832  eqabcbw  2834  eqabcb  2900  nfceqi  2919  ralbii2  3104  rexbii2  3105  r19.26-3  3123  r19.43  3130  r2allem  3150  r19.42v  3194  r19.32v  3195  reeanlem  3233  3reeanv  3235  cbvralvw  3240  cbvrexvw  3241  ralcom  3290  ralcomf  3300  rexcomf  3301  cbvralfw  3302  cbvralsvw  3313  cbvralf  3345  cbvrexf  3346  reu5  3367  rmobiia  3371  reubiia  3372  rmo5  3383  cbvrmovw  3386  cbvreuvw  3387  cbvrmow  3390  cbvreuw  3391  cbvreu  3404  cbvrmo  3405  rabid2f  3442  abv  3462  abvALT  3463  ceqsal  3487  ceqsalv  3489  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  reurab  3659  eueq  3666  reu2  3683  reu6  3684  reu3  3685  rmo4  3688  rmo3f  3692  2reu5  3716  cbvsbcw  3772  cbvsbcvw  3773  cbvsbc  3774  sbc3an  3803  rmo3  3836  rmoanim  3842  rmoanimALT  3843  cbvralcsf  3889  cbvrexcsf  3890  cbvreucsf  3891  eqss  3946  uniiunlem  4035  sspsstri  4054  compleq  4099  ssequn1  4132  unss  4136  rexun  4142  ralunb  4143  elin3  4152  inass  4173  ssin  4184  elsymdif  4204  nssinpss  4213  dfun2  4216  difin  4218  indi  4230  indifdi  4240  difin2  4247  eq0  4297  ssdif0  4314  inn0f  4319  inssdif0OLD  4323  ab0w  4328  ab0  4329  ab0orv  4332  abn0  4334  rabeq0w  4337  rabeq0  4338  disj3  4407  ssundif  4443  ralidmw  4472  dfif2  4484  eldifpr  4619  rexdifpr  4620  rexsns  4632  snprc  4678  reusn  4688  difsnpss  4770  tpss  4797  pwpr  4861  eluni2  4871  elunirab  4882  uniun  4890  unissb  4901  elintrab  4920  ssintrab  4931  intun  4940  iuncom  4959  iuncom4  4960  iunab  5010  ssiinf  5013  iunn0  5025  iinab  5026  iunin2  5029  iinun2  5031  iundif2  5032  iunun  5053  iunxun  5054  iunxiun  5057  sspwuni  5060  iinpw  5066  cbvdisj  5080  cbvdisjv  5081  disjor  5085  brun  5156  brin  5157  brdif  5158  dftr2  5214  dftr5  5216  intexrab  5311  inuni  5314  ssext  5429  pweqb  5431  otth2  5459  otthne  5462  propeqop  5484  vopelopabsb  5507  eqopab2bw  5527  eqopab2b  5531  pwin  5546  pwun  5548  dffr6  5611  elxp2  5679  otelxp  5699  xpiundi  5726  xpiundir  5727  poinxp  5736  soinxp  5737  frinxp  5738  seinxp  5739  weinxp  5740  reliun  5797  inopab  5810  difopab  5811  inxp  5812  raliunxp  5819  rexiunxp  5820  rexxpf  5827  iunxpf  5828  cnvco  5869  dmiun  5897  dmuni  5898  dm0rn0  5908  dm0rn0OLD  5909  dmres  6005  restidsing  6049  asymref  6110  codir  6114  qfto  6115  cnvopab  6131  cnvdif  6134  rniun  6139  dminss  6144  imainss  6145  cnvxp  6148  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  dmsnn0  6203  cnvcnvsn  6215  cnvresima  6226  resco  6246  imaco  6247  rnco  6248  rncoOLD  6249  coiun  6253  coass  6262  ressn  6283  cnviin  6284  cnvpo  6285  cnvso  6286  xpco  6287  opreu2reurex  6292  dfpo2  6294  imaindm  6297  dflim2  6416  funcnv  6602  funcnv3  6603  fncnv  6606  fun11  6607  imadif  6617  fnres  6659  dfmpt3  6666  mptfnf  6667  fnopabg  6669  fint  6754  fin  6755  fores  6799  dff1o3  6824  f1ompt  7104  fsn  7129  imaiun  7242  isocnv2  7332  isocnv3  7333  isores2  7334  isomin  7338  eqoprab2bw  7483  eqoprab2b  7484  elpwpwel  7766  sucexb  7803  onsucb  7813  dflim4  7844  fiun  7940  f1iun  7941  f11o  7944  opabex3d  7962  opabex3rd  7963  opabex3  7964  dfopab2  8049  dfoprab3s  8050  fmpox  8064  fparlem1  8109  fparlem2  8110  tpostpos  8244  frrlem9  8293  dfsmo2  8336  brwitnlem  8494  oarec  8549  naddasslem1  8683  naddasslem2  8684  qsid  8781  uniinqs  8797  mapval2  8879  mapsncnv  8900  elixp2  8908  ixpin  8930  brsdom  8980  brdom2  8988  xpassen  9069  brsdom2  9099  unfilem1  9275  fiint  9296  dfsup2  9414  supmo  9422  eqinf  9455  infmo  9467  brttrcl2  9693  rankc1  9852  cp  9893  isinfcard  10095  aceq1  10120  aceq2  10122  dfac5lem3  10128  dfac10b  10142  dfac12a  10151  dffin7-2  10400  dfacfin7  10401  fin1a2lem6  10407  iunfo  10547  konigthlem  10577  axgroth6  10837  axgroth3  10840  sstskm  10851  ltexprlem1  11045  gt0srpr  11087  ltpsrpr  11118  map2psrpr  11119  ltresr  11149  fimaxre3  12185  sup3  12196  supaddc  12206  supmul1  12208  elnn0z  12628  elznn0nn  12629  zmin  12993  xrnemnf  13168  xrnepnf  13169  dfrp2  13447  elioomnf  13497  elxrge0  13510  elfzuzb  13572  fzass4  13617  elfz2nn0  13673  elfzo2  13717  elfzo3  13732  lbfzo0  13755  fzo1lb  13769  fzind2  13844  nn0opthlem1  14332  hashgt23el  14489  cotr2g  15049  rexfiuz  15435  fsumcom2  15860  prodmo  16023  fprodcom2  16071  sinltx  16277  divalglem4  16486  divalglem10  16492  4sqlem12  17048  imasleval  17627  xpsfrnel  17648  xpscf  17651  isssc  17909  isffth2  18007  ispos2  18403  issubmgm  18804  ismhm  18893  issubmndb  18913  nsgacs  19285  isgim  19389  oppgcntz  19491  f1omvdco3  19576  pmtrprfvalrn  19615  efgrelexlemb  19877  pgpfac1  20209  pgpfac  20213  issrg  20327  opprsubg  20493  opprunit  20518  isirred2  20562  opprirred  20563  isrhm0  20617  opprnzrb  20682  opprdomnb  20878  isdomn4r  20880  drngprop  20907  isdrng3  20916  isdrng5  20917  opprdrng  20930  issdrg2  20961  isorng  21027  islss  21118  islbs  21260  isfieldidl  21449  isfieldidl2  21450  prmidl0  21541  unocv  21893  iunocv  21894  isbasis2g  23173  tgval2  23181  ntreq0  23302  isclo2  23313  cmpcov2  23615  is1stc2  23667  1stcelcls  23687  llyi  23700  unisngl  23753  txuni2  23791  xkobval  23812  hausdiag  23871  isfbas2  24061  elfg  24097  fbasrn  24110  fmfnfmlem3  24182  isfcls  24235  alexsubALTlem2  24274  istmd  24300  istgp  24303  istrg  24390  istdrg  24392  istdrg2  24404  isms2  24676  metuel2  24791  restmetu  24796  isngp  24822  isngp2  24823  isngp3  24824  elii1  25163  isncvsngp  25377  iscph  25398  isbn  25566  pmltpc  25678  ovolfcl  25694  finiunmbl  25772  iundisj  25776  dyaddisj  25824  vitalilem1  25836  ellimc3  26106  ig1pval3  26403  plyun0  26422  plydivex  26527  aannenlem2  26565  ellogrn  26796  atandm  27113  atandm3  27115  atans2  27168  elno3  27891  conway  28044  eqcuts2  28051  madeval2  28098  ons2ind  28540  tgjustf  28814  colinearalg  29367  axeuclid  29420  nbgrsym  29823  upgrtrls  30163  upgristrl  30164  dfpth2  30193  usgr2pth0  30230  iswwlks  30304  isclwwlk  30454  clwwlkneq0  30499  h2hlm  31461  issh  31689  chcon2i  31945  chcon1i  31946  chcon3i  31947  chnlei  31966  cmcm2i  32074  cmcm3i  32075  3oalem3  32145  pjdifnormii  32164  pjneli  32204  dfadj2  32366  cnvadj  32373  hhcno  32385  hhcnf  32386  eleigvec  32438  eleigvec2  32439  pjimai  32657  isst  32694  ishst  32695  cvnbtwn4  32770  chrelat4i  32854  2reucom  32955  reuxfrdf  32966  difrab2  32973  inpr0  33007  iunin1f  33031  disjnf  33043  cbvdisjf  33044  disjorf  33052  iundisjf  33062  disjexc  33066  xrdifh  33251  iundisjfi  33267  hashxpe  33278  pmtrprfv2  33528  xrnarchi  33624  isunit2  33679  opprnsg  33886  ccfldextdgrr  34182  cmpcref  34360  ordtconnlem1  34434  isrrext  34510  cntnevol  34739  ddemeas  34747  omssubaddlem  34810  omssubadd  34811  eulerpartleme  34874  eulerpartlemv  34875  eulerpartlemt0  34880  eulerpartlemgvv  34887  eulerpartlemn  34892  ballotlem2  35000  ballotlemodife  35009  oddprm2  35163  bnj257  35217  bnj268  35219  bnj290  35220  bnj312  35222  bnj89  35231  bnj887  35275  bnj976  35287  bnj1019  35289  bnj1146  35300  bnj1385  35341  bnj110  35367  bnj121  35379  bnj130  35383  bnj153  35389  bnj543  35402  bnj580  35422  bnj607  35425  bnj849  35434  bnj882  35435  bnj916  35442  bnj985v  35462  bnj985  35463  bnj1033  35478  bnj1083  35487  bnj1090  35488  bnj1128  35499  bnj1174  35512  bnj1228  35520  onvf1odlem1  35700  erdszelem1  35770  cvmliftlem15  35877  snmlval  35910  satfvsuclem2  35939  satfdm  35948  elmpst  36115  mpstrcl  36120  orbi2iALT  36264  untuni  36288  dfso3  36299  xpab  36305  dftr6  36330  coep  36331  coepr  36332  dffr5  36333  dfso2  36334  cnvco1  36338  cnvco2  36339  eldm3  36340  dfdm5  36352  dfrn5  36353  brsset  36466  idsset  36467  dfon3  36469  dfbigcup2  36476  dfom5b  36489  dffun10  36491  dfiota3  36500  fnimage  36506  brdomain  36510  brrange  36511  brimg  36514  brapply  36515  brcup  36516  brcap  36517  lemsuccf  36518  funpartlem  36521  brrestrict  36528  dfrecs2  36529  brub  36533  dffr7  36535  altopelaltxp  36556  ltnadd  36798  rmoeqi  36807  rmoeqbii  36808  reueqi  36809  reueqbii  36810  sbceqbii  36811  disjeq1i  36812  cbvralvw2  36846  cbvrexvw2  36847  cbvrmovw2  36848  cbvreuvw2  36849  cbvsbcvw2  36850  cbvdisjvw2  36855  trer  36935  filnetlem4  37000  df3nandALT1  37018  imnand2  37021  mh-unprimbi  37163  bj-dfbi5  37275  bj-bixor  37292  bj-dfsbc  37382  bj-nnfnt  37483  bj-csbsnlem  37646  bj-rcleqf  37769  bj-sscon  37773  bj-pw0ALT  37793  bj-restpw  37842  bj-opelidb1  37905  bj-imdiridlem  37937  bj-imdirco  37942  wl-df3xor2  38223  wl-3xorrot  38231  wl-3xorcoma  38232  wl-3xornot  38235  wl-df2-3mintru2  38239  wl-df3-3mintru2  38240  wl-df4-3mintru2  38241  wl-equsalvw  38301  wl-sb9v  38312  iundif1  38353  poimirlem25  38394  poimirlem26  38395  poimirlem30  38399  ismblfin  38410  mbfposadd  38416  itg2addnclem2  38421  ftc1anc  38450  inixp  38478  prdstotbnd  38544  heibor1lem  38559  isrngohom  38715  isidl  38764  isfldidl2  38819  isdmn3  38824  sbccom2lem  38872  scott0f  38917  triantru3  38984  vvdifopab  39013  brres2  39021  eldmqsres  39041  inxpss  39065  ref5  39067  n0el2  39083  dfsucmap3  39211  trcoss2  39322  dfeqvrel2  39422  dfeqvrel3  39423  redundeq1  39461  redundpbi1  39463  refrelredund4  39467  funALTVfun  39531  dfeldisj3  39559  dfeldisj5  39561  pet0  39666  petid  39668  petidres  39670  petinidres  39672  petxrnidres  39674  mpet  39701  petincnvepres  39711  pet  39713  pmapglbx  40642  lhpexle3  40885  cdleme25cv  41231  dicelval3  42053  diclspsn  42067  lcfls1c  42409  sn-axrep5v  43087  sn-iotalem  43091  psspwb  43098  redvmptabs  43235  eu6w  43522  moxfr  43537  fphpd  43657  uniel  44058  dflim6  44105  onsucf1olem  44111  dflim7  44114  omge2  44139  oenassex  44159  safesnsupfilb  44258  ifpim1  44309  ifpnot  44310  ifpid2  44311  ifpim2  44312  ifpxorcor  44316  ifpnot23  44318  ifpananb  44346  ifpnannanb  44347  ifpxorxorb  44351  rp-fakeinunass  44355  snen1g  44364  pren2  44393  alephiso2  44398  undmrnresiss  44444  cnvssco  44446  cotrintab  44454  cnviun  44490  imaiun1  44491  coiun1  44492  elintima  44493  frege133d  44605  frege54cor0a  44703  or3or  44863  andi3or  44864  ntrneik4w  44940  k0004lem1  44987  ismnuprim  45118  ismnushort  45125  undisjrab  45130  nzss  45141  pm10.541  45191  compab  45265  onfrALTlem5  45365  onfrALTlem5VD  45707  rext0  45761  wfaxun  45822  brpermmodel  45826  permaxrep  45829  permaxpow  45832  permac8prim  45837  eluni2f  45935  euabsneu  47916  aiotaexb  47977  aiotavb  47978  r19.32  47986  3an4ancom24  48157  ichn  48356  ichcom  48359  ichbi12i  48360  prproropf1olem0  48402  pairreueq  48410  clnbgrsym  48754  usgrexmpl2nb0  48947  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  usgrexmpl2nb3  48950  usgrexmpl2nb4  48951  usgrexmpl2nb5  48952  sgrp2sgrp  49143  isidom3  49260  islindeps  49383  elbigo  49481  reutruALT  49733  coxp  49761  tposres0  49803  catcinv  50325  isthincd2  50363  setrec1lem3  50615  elpg  50640  dfrals2  50719  alsbii  50729  ralsbii  50730  cbvals  50734  dfralseu2  50752  alseubii  50761  ralseubii  50762