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 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi2d  345  pm4.71  566  pm5.32ri  585  an31  660  pm4.14  818  or4  939  orimdi  943  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  1638  cadan  1639  cadcoma  1642  cadnot  1645  nic-axALT  1704  19.26-3an  1902  19.43OLD  1913  19.32v  1970  19.31v  1971  19.42v  1983  4exdistr  1991  cbvexvw  2067  exexw  2083  sb3an  2115  sbcom4  2123  sbbiiev  2127  excom  2197  sbal  2204  19.32  2269  19.31  2270  19.42  2272  equsalv  2303  sbex  2316  sbrim  2339  sbor  2341  sbbi  2342  cbvex2v  2376  eeeanv  2382  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  cbvabv  2833  cbvabw  2834  cbvab  2835  eqabcbw  2837  eqabcb  2903  nfceqi  2922  ralbii2  3107  rexbii2  3108  r19.26-3  3126  r19.43  3133  r2allem  3153  r19.42v  3197  r19.32v  3198  reeanlem  3236  3reeanv  3238  cbvralvw  3243  cbvrexvw  3244  ralcom  3293  ralcomf  3303  rexcomf  3304  cbvralfw  3305  cbvralsvw  3316  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  3447  abv  3467  abvALT  3468  ceqsal  3492  ceqsalv  3494  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  reurab  3664  eueq  3671  reu2  3688  reu6  3689  reu3  3690  rmo4  3693  rmo3f  3697  2reu5  3721  cbvsbcw  3777  cbvsbcvw  3778  cbvsbc  3779  sbc3an  3808  sbccomlemOLD  3823  rmo3  3842  rmoanim  3848  rmoanimALT  3849  cbvralcsf  3895  cbvrexcsf  3896  cbvreucsf  3897  eqss  3952  uniiunlem  4041  sspsstri  4060  compleq  4106  ssequn1  4139  unss  4143  rexun  4149  ralunb  4150  elin3  4159  inass  4180  ssin  4191  elsymdif  4211  nssinpss  4220  dfun2  4223  difin  4225  indi  4237  indifdi  4247  difin2  4254  eq0  4304  ssdif0  4321  inn0f  4326  inssdif0OLD  4330  ab0w  4335  ab0  4336  ab0orv  4339  abn0  4341  rabeq0w  4344  rabeq0  4345  disj3  4414  ssundif  4448  ralidmw  4477  dfif2  4489  eldifpr  4624  rexdifpr  4625  rexsns  4637  snprc  4683  reusn  4693  difsnpss  4775  tpss  4802  pwpr  4866  eluni2  4876  elunirab  4887  uniun  4895  unissb  4906  elintrab  4925  ssintrab  4936  intun  4945  iuncom  4964  iuncom4  4965  iunab  5016  ssiinf  5019  iunn0  5031  iinab  5032  iunin2  5035  iinun2  5037  iundif2  5038  iunun  5059  iunxun  5060  iunxiun  5063  sspwuni  5066  iinpw  5072  cbvdisj  5086  cbvdisjv  5087  disjor  5091  brun  5162  brin  5163  brdif  5164  dftr2  5220  dftr5  5222  intexrab  5317  inuni  5320  ssext  5435  pweqb  5437  otth2  5465  otthne  5468  propeqop  5490  vopelopabsb  5513  eqopab2bw  5533  eqopab2b  5537  pwin  5552  pwun  5554  dffr6  5617  elxp2  5685  otelxp  5705  xpiundi  5732  xpiundir  5733  poinxp  5742  soinxp  5743  frinxp  5744  seinxp  5745  weinxp  5746  reliun  5803  inopab  5816  difopab  5817  inxp  5818  raliunxp  5825  rexiunxp  5826  rexxpf  5833  iunxpf  5834  cnvco  5875  dmiun  5903  dmuni  5904  dm0rn0  5914  dm0rn0OLD  5915  dmres  6011  restidsing  6055  asymref  6116  codir  6120  qfto  6121  cnvopab  6137  cnvdif  6140  rniun  6145  dminss  6150  imainss  6151  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  dmsnn0  6208  cnvcnvsn  6220  cnvresima  6231  resco  6251  imaco  6252  rnco  6253  rncoOLD  6254  coiun  6258  coass  6267  ressn  6286  cnviin  6287  cnvpo  6288  cnvso  6289  xpco  6290  opreu2reurex  6295  dfpo2  6297  imaindm  6300  dflim2  6419  funcnv  6605  funcnv3  6606  fncnv  6609  fun11  6610  imadif  6620  fnres  6662  dfmpt3  6669  mptfnf  6670  fnopabg  6672  fint  6757  fin  6758  fores  6802  dff1o3  6827  f1ompt  7106  fsn  7131  imaiun  7243  isocnv2  7329  isocnv3  7330  isores2  7331  isomin  7335  eqoprab2bw  7480  eqoprab2b  7481  elpwpwel  7762  sucexb  7799  onsucb  7809  dflim4  7840  fiun  7936  f1iun  7937  f11o  7940  opabex3d  7958  opabex3rd  7959  opabex3  7960  dfopab2  8045  dfoprab3s  8046  fmpox  8060  fparlem1  8103  fparlem2  8104  tpostpos  8238  frrlem9  8287  dfsmo2  8330  brwitnlem  8488  oarec  8543  naddasslem1  8677  naddasslem2  8678  qsid  8775  uniinqs  8791  mapval2  8866  mapsncnv  8887  elixp2  8895  ixpin  8917  brsdom  8967  brdom2  8975  xpassen  9055  brsdom2  9085  unfilem1  9261  fiint  9282  dfsup2  9400  supmo  9408  eqinf  9441  infmo  9453  brttrcl2  9679  rankc1  9838  cp  9873  isinfcard  10072  aceq1  10097  aceq2  10099  dfac5lem3  10105  dfac10b  10119  dfac12a  10128  dffin7-2  10377  dfacfin7  10378  fin1a2lem6  10384  iunfo  10518  konigthlem  10548  axgroth6  10808  axgroth3  10811  sstskm  10822  ltexprlem1  11016  gt0srpr  11058  ltpsrpr  11089  map2psrpr  11090  ltresr  11120  fimaxre3  12156  sup3  12167  supaddc  12177  supmul1  12179  elnn0z  12599  elznn0nn  12600  zmin  12963  xrnemnf  13137  xrnepnf  13138  dfrp2  13416  elioomnf  13466  elxrge0  13479  elfzuzb  13541  fzass4  13586  elfz2nn0  13642  elfzo2  13686  elfzo3  13701  lbfzo0  13724  fzo1lb  13738  fzind2  13813  nn0opthlem1  14300  hashgt23el  14457  cotr2g  15009  rexfiuz  15395  fsumcom2  15821  prodmo  15986  fprodcom2  16034  sinltx  16240  divalglem4  16449  divalglem10  16455  4sqlem12  17011  imasleval  17590  xpsfrnel  17611  xpscf  17614  isssc  17872  isffth2  17970  ispos2  18366  issubmgm  18755  ismhm  18838  issubmndb  18858  nsgacs  19223  isgim  19327  oppgcntz  19429  f1omvdco3  19514  pmtrprfvalrn  19553  efgrelexlemb  19815  pgpfac1  20147  pgpfac  20151  issrg  20265  opprsubg  20430  opprunit  20455  isirred2  20499  opprirred  20500  isrhm0  20554  opprnzrb  20619  opprdomnb  20815  isdomn4r  20817  drngprop  20844  isdrng3  20853  isdrng5  20854  opprdrng  20867  issdrg2  20898  isorng  20964  islss  21055  islbs  21197  isfieldidl  21386  isfieldidl2  21387  prmidl0  21478  unocv  21830  iunocv  21831  isbasis2g  23105  tgval2  23113  ntreq0  23234  isclo2  23245  cmpcov2  23547  is1stc2  23599  1stcelcls  23618  llyi  23631  unisngl  23684  txuni2  23722  xkobval  23743  hausdiag  23802  isfbas2  23992  elfg  24028  fbasrn  24041  fmfnfmlem3  24113  isfcls  24166  alexsubALTlem2  24205  istmd  24231  istgp  24234  istrg  24321  istdrg  24323  istdrg2  24335  isms2  24607  metuel2  24722  restmetu  24727  isngp  24753  isngp2  24754  isngp3  24755  elii1  25094  isncvsngp  25308  iscph  25329  isbn  25497  pmltpc  25609  ovolfcl  25625  finiunmbl  25703  iundisj  25707  dyaddisj  25755  vitalilem1  25767  ellimc3  26038  ig1pval3  26335  plyun0  26354  plydivex  26458  aannenlem2  26492  ellogrn  26724  atandm  27041  atandm3  27043  atans2  27096  elno3  27819  conway  27972  eqcuts2  27979  madeval2  28026  ons2ind  28468  tgjustf  28742  colinearalg  29260  axeuclid  29313  nbgrsym  29713  upgrtrls  30049  upgristrl  30050  dfpth2  30078  usgr2pth0  30114  iswwlks  30185  isclwwlk  30335  clwwlkneq0  30380  h2hlm  31332  issh  31560  chcon2i  31816  chcon1i  31817  chcon3i  31818  chnlei  31837  cmcm2i  31945  cmcm3i  31946  3oalem3  32016  pjdifnormii  32035  pjneli  32075  dfadj2  32237  cnvadj  32244  hhcno  32256  hhcnf  32257  eleigvec  32309  eleigvec2  32310  pjimai  32528  isst  32565  ishst  32566  cvnbtwn4  32641  chrelat4i  32725  2reucom  32826  reuxfrdf  32837  difrab2  32844  inpr0  32878  iunin1f  32902  disjnf  32915  cbvdisjf  32916  disjorf  32924  iundisjf  32934  disjexc  32938  xrdifh  33125  iundisjfi  33141  hashxpe  33152  pmtrprfv2  33408  xrnarchi  33504  isunit2  33559  opprnsg  33766  ccfldextdgrr  34062  cmpcref  34240  ordtconnlem1  34314  isrrext  34390  cntnevol  34618  ddemeas  34626  omssubaddlem  34689  omssubadd  34690  eulerpartleme  34753  eulerpartlemv  34754  eulerpartlemt0  34759  eulerpartlemgvv  34766  eulerpartlemn  34771  ballotlem2  34879  ballotlemodife  34888  oddprm2  35042  bnj257  35096  bnj268  35098  bnj290  35099  bnj312  35101  bnj89  35110  bnj887  35154  bnj976  35166  bnj1019  35168  bnj1146  35179  bnj1385  35220  bnj110  35246  bnj121  35258  bnj130  35262  bnj153  35268  bnj543  35281  bnj580  35301  bnj607  35304  bnj849  35313  bnj882  35314  bnj916  35321  bnj985v  35341  bnj985  35342  bnj1033  35357  bnj1083  35366  bnj1090  35367  bnj1128  35378  bnj1174  35391  bnj1228  35399  onvf1odlem1  35587  erdszelem1  35683  cvmliftlem15  35790  snmlval  35823  satfvsuclem2  35852  satfdm  35861  elmpst  36028  mpstrcl  36033  orbi2iALT  36177  untuni  36201  dfso3  36212  xpab  36218  dftr6  36243  coep  36244  coepr  36245  dffr5  36246  dfso2  36247  cnvco1  36251  cnvco2  36252  eldm3  36253  dfdm5  36265  dfrn5  36266  brsset  36379  idsset  36380  dfon3  36382  dfbigcup2  36389  dfom5b  36402  dffun10  36404  dfiota3  36413  fnimage  36419  brdomain  36423  brrange  36424  brimg  36427  brapply  36428  brcup  36429  brcap  36430  lemsuccf  36431  funpartlem  36434  brrestrict  36441  dfrecs2  36442  brub  36446  altopelaltxp  36468  ltnadd  36695  rmoeqi  36699  rmoeqbii  36700  reueqi  36701  reueqbii  36702  sbceqbii  36703  disjeq1i  36704  cbvralvw2  36738  cbvrexvw2  36739  cbvrmovw2  36740  cbvreuvw2  36741  cbvsbcvw2  36742  cbvdisjvw2  36747  trer  36827  filnetlem4  36892  df3nandALT1  36910  imnand2  36913  mh-unprimbi  37055  bj-dfbi5  37167  bj-bixor  37184  bj-dfsbc  37274  bj-nnfnt  37375  bj-csbsnlem  37538  bj-rcleqf  37661  bj-sscon  37665  bj-pw0ALT  37685  bj-restpw  37734  bj-opelidb1  37797  bj-imdiridlem  37829  bj-imdirco  37834  wl-df3xor2  38115  wl-3xorrot  38123  wl-3xorcoma  38124  wl-3xornot  38127  wl-df2-3mintru2  38131  wl-df3-3mintru2  38132  wl-df4-3mintru2  38133  wl-equsalvw  38193  wl-sb9v  38204  iundif1  38245  poimirlem25  38296  poimirlem26  38297  poimirlem30  38301  ismblfin  38312  mbfposadd  38318  itg2addnclem2  38323  ftc1anc  38352  inixp  38379  prdstotbnd  38445  heibor1lem  38460  isrngohom  38616  isidl  38665  isfldidl2  38720  isdmn3  38725  sbccom2lem  38773  triantru3  38885  vvdifopab  38914  brres2  38922  eldmqsres  38942  inxpss  38966  ref5  38968  n0el2  38984  dfsucmap3  39112  trcoss2  39223  dfeqvrel2  39323  dfeqvrel3  39324  redundeq1  39362  redundpbi1  39364  refrelredund4  39368  funALTVfun  39432  dfeldisj3  39460  dfeldisj5  39462  pet0  39567  petid  39569  petidres  39571  petinidres  39573  petxrnidres  39575  mpet  39602  petincnvepres  39612  pet  39614  pmapglbx  40543  lhpexle3  40786  cdleme25cv  41132  dicelval3  41954  diclspsn  41968  lcfls1c  42310  sn-axrep5v  42988  sn-iotalem  42992  psspwb  42999  redvmptabs  43121  eu6w  43408  moxfr  43423  fphpd  43543  uniel  43944  dflim6  43991  onsucf1olem  43997  dflim7  44000  omge2  44025  oenassex  44045  safesnsupfilb  44144  ifpim1  44195  ifpnot  44196  ifpid2  44197  ifpim2  44198  ifpxorcor  44202  ifpnot23  44204  ifpananb  44232  ifpnannanb  44233  ifpxorxorb  44237  rp-fakeinunass  44241  snen1g  44250  pren2  44279  alephiso2  44284  undmrnresiss  44330  cnvssco  44332  cotrintab  44340  cnviun  44376  imaiun1  44377  coiun1  44378  elintima  44379  frege133d  44491  frege54cor0a  44589  or3or  44749  andi3or  44750  ntrneik4w  44826  k0004lem1  44873  ismnuprim  45004  ismnushort  45011  undisjrab  45016  nzss  45027  pm10.541  45077  compab  45151  onfrALTlem5  45251  onfrALTlem5VD  45593  rext0  45647  wfaxun  45708  brpermmodel  45712  permaxrep  45715  permaxpow  45718  permac8prim  45723  eluni2f  45821  euabsneu  47765  aiotaexb  47826  aiotavb  47827  r19.32  47835  3an4ancom24  48006  ichn  48205  ichcom  48208  ichbi12i  48209  prproropf1olem0  48251  pairreueq  48259  clnbgrsym  48603  usgrexmpl2nb0  48796  usgrexmpl2nb1  48797  usgrexmpl2nb2  48798  usgrexmpl2nb3  48799  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  sgrp2sgrp  48993  isidom3  49110  islindeps  49233  elbigo  49331  reutruALT  49583  coxp  49611  tposres0  49655  catcinv  50177  isthincd2  50215  setrec1lem3  50467  elpg  50492  dfrals2  50568  alsbii  50578  ralsbii  50579  cbvals  50583  dfralseu2  50601  alseubii  50610  ralseubii  50611