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  1454  an6  1475  3or6  1477  an3andi  1514  an33rean  1515  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  1918  19.32v  1975  19.31v  1976  19.42v  1988  4exdistr  1996  cbvexvw  2072  exexw  2088  sb3an  2120  sbcom4  2128  sbbiiev  2132  excom  2202  sbal  2209  19.32  2273  19.31  2274  19.42  2276  equsalv  2305  sbex  2318  sbrim  2341  sbor  2343  sbbi  2344  cbvex2v  2377  eeeanv  2383  sbnf2  2390  cbvsbvf  2395  cbvex2  2444  equsal  2449  dfsb3  2526  mo4  2594  eu6  2602  dfeu  2623  sb8eulem  2626  sb8mo  2629  cbvmovw  2630  cbvmow  2631  cbveuvw  2633  cbveuw  2634  cbveuALT  2636  eu1  2638  sbmo  2642  abbib  2832  cbvabv  2834  cbvabw  2835  cbvab  2836  eqabcbw  2838  eqabcb  2904  nfceqi  2923  ralbii2  3108  rexbii2  3109  r19.26-3  3127  r19.43  3134  r2allem  3154  r19.42v  3198  r19.32v  3199  reeanlem  3237  3reeanv  3239  cbvralvw  3244  cbvrexvw  3245  ralcom  3294  ralcomf  3304  rexcomf  3305  cbvralfw  3306  cbvralsvw  3317  cbvralf  3349  cbvrexf  3350  reu5  3371  rmobiia  3375  reubiia  3376  rmo5  3387  cbvrmovw  3390  cbvreuvw  3391  cbvrmow  3394  cbvreuw  3395  cbvreu  3408  cbvrmo  3409  rabid2f  3446  abv  3466  abvALT  3467  ceqsal  3491  ceqsalv  3493  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  reurab  3662  eueq  3669  reu2  3686  reu6  3687  reu3  3688  rmo4  3691  rmo3f  3695  2reu5  3719  cbvsbcw  3775  cbvsbcvw  3776  cbvsbc  3777  sbc3an  3806  rmo3  3840  rmoanim  3846  rmoanimALT  3847  cbvralcsf  3893  cbvrexcsf  3894  cbvreucsf  3895  eqss  3928  uniiunlem  4015  sspsstri  4036  compleq  4091  elin3  4106  inass  4127  ssin  4138  ssequn1  4187  unss  4191  rexun  4197  ralunb  4198  elsymdif  4206  nssinpss  4215  dfun2  4218  difin  4220  indi  4232  indifdi  4242  difin2  4249  eq0  4300  ssdif0  4317  inn0f  4322  inssdif0OLD  4326  ab0w  4331  ab0  4332  ab0orv  4335  abn0  4337  rabeq0w  4340  rabeq0  4341  disj3  4410  ssundif  4446  ralidmw  4475  dfif2  4487  eldifpr  4620  rexdifpr  4621  rexsns  4633  snprc  4680  reusn  4690  difsnpss  4772  tpss  4797  pwpr  4833  eluni2  4876  elunirab  4887  uniun  4895  unissb  4906  elintrab  4925  ssintrab  4936  intun  4945  iuncom  4964  iuncom4  4965  iunab  5015  ssiinf  5018  iunn0  5030  iinab  5031  iunin2  5034  iinun2  5036  iundif2  5037  iunun  5058  iunxun  5059  iunxiun  5062  sspwuni  5065  iinpw  5071  cbvdisj  5085  cbvdisjv  5086  disjor  5090  brun  5162  brin  5163  brdif  5164  dftr2  5220  dftr5  5222  intexrab  5315  inuni  5318  ssext  5429  pweqb  5431  otth2  5459  otthne  5462  propeqop  5486  vopelopabsb  5510  eqopab2bw  5530  eqopab2b  5534  pwin  5549  pwun  5551  dffr6  5614  elxp2  5682  otelxp  5702  xpiundi  5729  xpiundir  5730  poinxp  5740  soinxp  5741  frinxp  5742  seinxp  5743  weinxp  5744  reliun  5803  inopab  5817  difopab  5818  inxp  5819  raliunxp  5826  rexiunxp  5827  rexxpf  5835  iunxpf  5836  cnvco  5879  dmiun  5907  dmuni  5908  dm0rn0  5918  dm0rn0OLD  5919  dmres  6020  restidsing  6063  asymref  6128  codir  6132  qfto  6133  cnvopab  6149  cnvdif  6152  rniun  6157  dminss  6161  imainss  6162  cnvxp  6165  difxp  6173  xpdifid  6177  xpdifcnvepel  6178  dmsnn0  6227  cnvcnvsn  6239  cnvresima  6250  resco  6270  imaco  6271  rnco  6272  rncoOLD  6273  coiun  6277  coassOLD  6291  ressn  6312  cnviin  6313  cnvpo  6314  cnvso  6315  xpco  6318  opreu2reurex  6323  dfpo2  6325  imaindm  6328  dflim2  6447  funcnv  6639  funcnv3  6640  fncnv  6643  fun11  6644  imadif  6654  fnres  6696  dfmpt3  6703  mptfnf  6704  fnopabg  6706  fint  6791  fin  6792  fores  6836  dff1o3  6861  f1ompt  7143  fsn  7168  imaiun  7280  isocnv2  7370  isocnv3  7371  isores2  7372  isomin  7376  eqoprab2bw  7521  eqoprab2b  7522  elpwpwel  7813  sucexb  7852  onsucb  7862  dflim4  7893  fiun  7989  f1iun  7990  f11o  7993  opabex3d  8011  opabex3rd  8012  opabex3  8013  dfopab2  8098  dfoprab3s  8099  fmpox  8113  fparlem1  8160  fparlem2  8161  suppvalbr  8218  tpostpos  8301  frrlem9  8350  dfsmo2  8393  brwitnlem  8553  oarec  8608  naddasslem1  8742  naddasslem2  8743  qsid  8840  uniinqs  8856  mapval2  8938  mapsncnv  8959  elixp2  8967  ixpin  8989  brsdom  9039  brdom2  9047  xpassen  9128  brsdom2  9158  unfilem1  9335  fiint  9356  dfsup2  9473  supmo  9481  eqinf  9514  infmo  9526  brttrcl2  9752  rankc1  9924  cp  9991  setrec1lem3  10006  isinfcard  10210  aceq1  10235  aceq2  10237  dfac5lem3  10243  dfac10b  10257  dfac12a  10266  dffin7-2  10515  dfacfin7  10516  fin1a2lem6  10522  iunfo  10662  konigthlem  10692  axgroth6  10952  axgroth3  10955  sstskm  10966  ltexprlem1  11160  gt0srpr  11202  ltpsrpr  11233  map2psrpr  11234  ltresr  11264  fimaxre3  12303  sup3  12314  supaddc  12324  supmul1  12326  elnn0z  12746  elznn0nn  12747  zmin  13111  xrnemnf  13286  xrnepnf  13287  dfrp2  13565  elioomnf  13615  elxrge0  13628  elfzuzb  13690  fzass4  13736  elfz2nn0  13792  elfzo2  13836  elfzo3  13851  lbfzo0  13874  fzo1lb  13888  fzind2  13963  nn0opthlem1  14453  hashgt23el  14610  cotr2g  15172  rexfiuz  15559  fsumcom2  15984  prodmo  16147  fprodcom2  16195  sinltx  16401  divalglem4  16610  divalglem10  16616  4sqlem12  17178  imasleval  17763  xpsfrnel  17784  xpscf  17787  isssc  18045  isffth2  18143  ispos2  18539  issubmgm  18941  ismhm  19030  issubmndb  19050  nsgacs  19422  isgim  19526  oppgcntz  19629  f1omvdco3  19714  pmtrprfvalrn  19753  efgrelexlemb  20015  pgpfac1  20347  pgpfac  20351  issrg  20465  dfring3  20569  opprsubg  20633  opprunit  20658  isirred2  20702  opprirred  20703  isrhm0  20757  dfric2  20808  opprnzrb  20823  opprdomnb  21019  isdomn4r  21021  drngprop  21049  isdrng3  21058  isdrng5  21059  opprdrng  21072  issdrg2  21103  isorng  21169  islss  21260  islbs  21402  isfieldidl  21591  isfieldidl2  21592  prmidl0  21685  unocv  22041  iunocv  22042  isbasis2g  23321  tgval2  23329  ntreq0  23450  isclo2  23461  cmpcov2  23763  is1stc2  23815  1stcelcls  23835  llyi  23848  unisngl  23901  txuni2  23939  xkobval  23960  hausdiag  24019  isfbas2  24209  elfg  24245  fbasrn  24258  fmfnfmlem3  24330  isfcls  24383  alexsubALTlem2  24422  istmd  24448  istgp  24451  istrg  24538  istdrg  24540  istdrg2  24552  isms2  24824  metuel2  24939  restmetu  24944  isngp  24970  isngp2  24971  isngp3  24972  elii1  25311  isncvsngp  25525  iscph  25546  isbn  25714  pmltpc  25826  ovolfcl  25842  finiunmbl  25920  iundisj  25924  dyaddisj  25972  vitalilem1  25984  ellimc3  26254  ig1pval3  26551  plyun0  26570  plydivex  26673  aannenlem2  26713  ellogrn  26944  atandm  27261  atandm3  27263  atans2  27316  elno3  28069  conway  28222  eqcuts2  28229  madeval2  28276  ons2ind  28718  tgjustf  28992  colinearalg  29545  axeuclid  29598  nbgrsym  30001  upgrtrls  30341  upgristrl  30342  dfpth2  30371  usgr2pth0  30408  iswwlks  30482  isclwwlk  30632  clwwlkneq0  30677  h2hlm  31639  issh  31867  chcon2i  32123  chcon1i  32124  chcon3i  32125  chnlei  32144  cmcm2i  32252  cmcm3i  32253  3oalem3  32323  pjdifnormii  32342  pjneli  32382  dfadj2  32544  cnvadj  32551  hhcno  32563  hhcnf  32564  eleigvec  32616  eleigvec2  32617  pjimai  32835  isst  32872  ishst  32873  cvnbtwn4  32948  chrelat4i  33032  2reucom  33175  reuxfrdf  33186  difrab2  33193  inpr0  33226  iunin1f  33250  disjnf  33262  cbvdisjf  33263  disjorf  33271  iundisjf  33281  disjexc  33285  xrdifh  33468  iundisjfi  33484  hashxpe  33495  pmtrprfv2  33748  xrnarchi  33844  isunit2  33899  opprnsg  34112  ccfldextdgrr  34415  cmpcref  34593  ordtconnlem1  34667  isrrext  34743  cntnevol  34972  ddemeas  34980  omssubaddlem  35042  omssubadd  35043  eulerpartleme  35106  eulerpartlemv  35107  eulerpartlemt0  35112  eulerpartlemgvv  35119  eulerpartlemn  35124  ballotlem2  35232  ballotlemodife  35241  oddprm2  35395  bnj257  35449  bnj268  35451  bnj290  35452  bnj312  35454  bnj89  35463  bnj887  35507  bnj976  35519  bnj1019  35521  bnj1146  35532  bnj1385  35573  bnj110  35599  bnj121  35611  bnj130  35615  bnj153  35621  bnj543  35634  bnj580  35654  bnj607  35657  bnj849  35666  bnj882  35667  bnj916  35674  bnj985v  35694  bnj985  35695  bnj1033  35710  bnj1083  35719  bnj1090  35720  bnj1128  35731  bnj1174  35744  bnj1228  35752  reu6f  35820  fwfffun  35828  fwfffunres  35829  0elscott  35878  onvf1odlem1  36072  srepdflem1  36126  srepdflem2  36127  erdszelem1  36164  cvmliftlem15  36271  snmlval  36304  satfvsuclem2  36333  satfdm  36342  elmpst  36509  mpstrcl  36514  orbi2iALT  36658  elpsseu  36674  untuni  36689  dfso3  36700  xpab  36706  dftr6  36731  coep  36732  coepr  36733  dffr5  36734  dfso2  36735  cnvco1  36739  cnvco2  36740  eldm3  36741  dfdm5  36752  dfrn5  36753  brsset  36866  idsset  36867  dfon3  36869  dfbigcup2  36876  dfom5b  36889  dffun10  36891  dfiota3  36900  fnimage  36906  brdomain  36910  brrange  36911  brimg  36914  brapply  36915  brcup  36916  brcap  36917  lemsuccf  36918  funpartlem  36921  brrestrict  36928  dfrecs2  36929  brub  36933  dffr7  36935  altopelaltxp  36956  ltnadd  37182  rmoeqi  37191  rmoeqbii  37192  reueqi  37193  reueqbii  37194  sbceqbii  37195  disjeq1i  37196  cbvralvw2  37230  cbvrexvw2  37231  cbvrmovw2  37232  cbvreuvw2  37233  cbvsbcvw2  37234  cbvdisjvw2  37239  trer  37319  filnetlem4  37384  df3nandALT1  37402  imnand2  37405  mh-unprimbi  37547  bj-dfbi5  37659  bj-bixor  37676  bj-dfsbc  37766  bj-nnfnt  37867  bj-csbsnlem  38030  bj-rcleqf  38153  bj-sscon  38157  bj-dfres2  38185  bj-pw0ALT  38234  bj-restpw  38283  bj-opelidb1  38342  bj-imdiridlem  38374  bj-imdirco  38379  wl-df3xor2  38660  wl-3xorrot  38668  wl-3xorcoma  38669  wl-3xornot  38672  wl-df2-3mintru2  38676  wl-df3-3mintru2  38677  wl-df4-3mintru2  38678  wl-equsalvw  38738  wl-sb9v  38749  iundif1  38790  poimirlem25  38831  poimirlem26  38832  poimirlem30  38836  ismblfin  38847  mbfposadd  38853  itg2addnclem2  38858  ftc1anc  38887  inixp  38930  prdstotbnd  38994  heibor1lem  39009  isrngohom  39165  isidl  39214  isfldidl2  39269  isdmn3  39274  sbccom2lem  39322  scott0f  39367  triantru3  39434  vvdifopab  39463  brres2  39471  eldmqsres  39491  inxpss  39515  ref5  39517  n0el2  39533  dfsucmap3  39661  trcoss2  39772  dfeqvrel2  39872  dfeqvrel3  39873  redundeq1  39911  redundpbi1  39913  refrelredund4  39917  funALTVfun  39981  dfeldisj3  40009  dfeldisj5  40011  pet0  40116  petid  40118  petidres  40120  petinidres  40122  petxrnidres  40124  mpet  40151  petincnvepres  40161  pet  40163  pmapglbx  41092  lhpexle3  41335  cdleme25cv  41681  dicelval3  42503  diclspsn  42517  lcfls1c  42859  sn-axrep5v  43538  sn-iotalem  43542  psspwb  43549  redvmptabs  43677  eu6w  43953  moxfr  43969  fphpd  44089  uniel  44480  dflim6  44527  onsucf1olem  44533  dflim7  44536  omge2  44561  oenassex  44581  safesnsupfilb  44680  ifpim1  44731  ifpnot  44732  ifpid2  44733  ifpim2  44734  ifpxorcor  44738  ifpnot23  44740  ifpananb  44768  ifpnannanb  44769  ifpxorxorb  44773  rp-fakeinunass  44777  snen1g  44786  pren2  44815  alephiso2  44820  undmrnresiss  44865  cnvssco  44867  cotrintab  44875  cnviun  44911  imaiun1  44912  coiun1  44913  elintima  44914  frege133d  45026  frege54cor0a  45124  or3or  45284  andi3or  45285  ntrneik4w  45361  k0004lem1  45408  ismnuprim  45539  ismnushort  45546  undisjrab  45551  nzss  45562  pm10.541  45612  compab  45685  onfrALTlem5  45785  onfrALTlem5VD  46127  rext0  46181  wfaxun  46253  brpermmodel  46257  permaxrep  46260  permaxpow  46263  permac8prim  46268  eluni2f  46391  euabsneu  48371  aiotaexb  48432  aiotavb  48433  r19.32  48442  3an4ancom24  48612  ichn  48811  ichcom  48814  ichbi12i  48815  prproropf1olem0  48857  pairreueq  48865  clnbgrsym  49209  usgrexmpl2nb0  49402  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  sgrp2sgrp  49598  gzilaz  49735  isidom3  49773  islindeps  49896  elbigo  49994  reutruALT  50246  coxp  50275  tposres0  50321  isnat3  50673  catcinv  50865  isthincd2  50903  elpg  51213  dfrals2  51314  alsbii  51324  ralsbii  51325  cbvals  51329  dfralseu2  51347  alseubii  51356  ralseubii  51357