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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bibi2d  343  pm4.71  558  pm5.32ri  576  an31  645  pm4.14  804  or4  924  orimdi  928  orbidi  950  ordi  1003  ordir  1004  andir  1006  dfbi3  1047  dfifp7  1067  ifpdfbi  1068  ifpn  1071  ifpnOLD  1072  3orrot  1091  3orcoma  1092  3ioran  1105  3ianor  1106  3anbi123i  1154  3orbi123i  1155  an6  1444  3or6  1446  an33rean  1482  an33reanOLD  1483  nancom  1491  xorcomOLD  1510  xorass  1511  xorbi12iOLD  1521  anxordi  1523  norcomOLD  1528  norass  1535  hadbi  1599  hadcoma  1600  hadcomaOLD  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1677  nfnbiOLD  1859  19.26-3an  1876  19.43OLD  1887  19.32v  1944  19.31v  1945  19.42v  1958  4exdistr  1966  cbvexvw  2041  exexw  2055  sb3an  2085  sbcom4  2093  sbcom3vv  2099  sbal  2160  excom  2163  19.32  2227  19.31  2228  19.42  2230  equsalv  2260  sbex  2279  sbrim  2302  sbor  2305  sbbi  2306  cbvex2v  2343  eeeanv  2349  sbnf2  2357  sbievg  2362  cbvex2  2413  equsal  2418  dfsb3  2499  mo4  2567  eu6  2575  eubii  2586  dfeu  2596  sb8eulem  2599  sb8mo  2602  cbvmovw  2603  cbvmow  2604  cbvmowOLD  2605  cbveuvw  2607  cbveuw  2608  cbveuALT  2611  eu1  2613  sbmo  2617  cbvabv  2812  cbvabw  2813  cbvabwOLD  2814  cbvab  2815  abeq1  2874  nfceqi  2905  sbabelOLD  2943  ralbii2  3091  r19.21vOLD  3115  r2allem  3118  ralcom4OLD  3166  ralcom  3167  rexbii2  3180  r19.32v  3271  r19.41v  3277  r19.41  3278  r19.42v  3280  r19.43  3281  ralcomf  3284  rexcomf  3285  reeanlem  3293  3reeanv  3296  2ralorOLD  3298  reuanid  3299  rmoanid  3300  rabid2f  3314  rabid2OLD  3316  rabbi  3317  reubiia  3325  rmobiia  3331  moel  3359  moelOLD  3360  reu5  3362  rmo5  3366  cbvralfw  3369  cbvralfwOLD  3370  cbvralf  3372  cbvrexf  3373  cbvrmow  3376  cbvreuw  3377  cbvreuwOLD  3378  cbvrmowOLD  3379  cbvreu  3382  cbvrmo  3383  cbvralvw  3384  cbvrexvw  3385  cbvrmovw  3386  cbvreuvw  3387  abv  3444  abvALT  3445  cgsex4g  3477  ceqsex3v  3485  ceqsex4v  3486  ceqsex8v  3488  eueq  3644  reu2  3661  reu6  3662  reu3  3663  rmo4  3666  rmo3f  3670  2reu5  3694  cbvsbcw  3751  cbvsbcvw  3752  cbvsbc  3753  sbccomlem  3804  rmo3  3823  rmoanim  3828  rmoanimALT  3829  cbvralcsf  3878  cbvrexcsf  3879  cbvreucsf  3880  dfss2  3908  eqss  3937  uniiunlem  4020  sspsstri  4038  compleq  4083  ssequn1  4115  unss  4119  rexun  4125  ralunb  4126  elin3  4135  inass  4154  ssin  4165  elsymdif  4182  nssinpss  4191  dfun2  4194  difin  4196  indi  4208  indifdi  4218  indifdirOLD  4220  ssdif0  4298  inssdif0  4304  abn0  4315  rabeq0w  4318  rabeq0  4319  disj  4382  disj3  4388  ssundif  4419  ralidmw  4439  dfif2  4462  eldifpr  4594  rexsns  4606  snprc  4654  reusn  4664  difsnpss  4741  tpss  4769  dfopif  4801  pwpr  4834  eluni2  4844  elunirab  4856  uniun  4865  unissb  4874  elintrab  4892  ssintrab  4903  intun  4912  intprOLD  4915  iuncom  4932  iuncom4  4933  iunab  4982  ssiinf  4985  iunn0  4997  iinab  4998  iunin2  5001  iinun2  5003  iundif2  5004  iunun  5023  iunxun  5024  iunxiun  5027  sspwuni  5030  iinpw  5036  cbvdisj  5050  disjor  5055  brun  5126  brin  5127  brdif  5128  dftr2  5194  intexrab  5265  inuni  5268  ssext  5371  pweqb  5373  otth2  5399  propeqop  5422  vopelopabsb  5443  eqopab2bw  5462  eqopab2b  5466  pwin  5484  pwun  5488  dffr6  5548  elxp2  5614  xpiundi  5658  xpiundir  5659  poinxp  5668  soinxp  5669  frinxp  5670  seinxp  5671  weinxp  5672  inopab  5741  difopab  5742  difopabOLD  5743  raliunxp  5751  rexiunxp  5752  rexxpf  5759  iunxpf  5760  cnvco  5797  dmiun  5825  dmuni  5826  dm0rn0  5837  dmres  5916  restidsing  5965  cnvsym  6024  asymref  6026  codir  6030  qfto  6031  cnvopab  6047  cnvdif  6052  rniun  6056  dminss  6061  imainss  6062  difxp  6072  xpdifid  6076  dmsnn0  6115  cnvcnvsn  6127  cnvresima  6138  resco  6158  imaco  6159  rnco  6160  coiun  6164  coass  6173  ressn  6192  cnviin  6193  cnvpo  6194  cnvso  6195  xpco  6196  opreu2reurex  6201  dfpo2  6203  dflim2  6326  unisuc  6346  funcnv  6510  funcnv3  6511  fncnv  6514  fun11  6515  imadif  6525  fnres  6568  dfmpt3  6576  mptfnf  6577  fnopabg  6579  fint  6662  fin  6663  fores  6707  dff1o3  6731  f1ompt  6994  fsn  7016  imaiun  7127  isocnv2  7211  isocnv3  7212  isores2  7213  isomin  7217  eqoprab2bw  7354  eqoprab2b  7355  elpwpwel  7626  sucexb  7663  sucelon  7673  dflim4  7704  fiun  7794  f1iun  7795  f11o  7798  opabex3d  7817  opabex3rd  7818  opabex3  7819  dfopab2  7901  dfoprab3s  7902  fmpox  7916  fparlem1  7961  fparlem2  7962  fsplitOLD  7967  suppvalbr  7990  tpostpos  8071  frrlem9  8119  wfrlem8OLD  8156  wfrfunOLD  8159  dfsmo2  8187  brwitnlem  8346  oarec  8402  qsid  8581  uniinqs  8595  mapval2  8669  mapsncnv  8690  elixp2  8698  ixpin  8720  brsdom  8772  brdom2  8779  xpassen  8862  brsdom2  8893  dif1en  8954  unfilem1  9087  fiint  9100  dfsup2  9212  supmo  9220  eqinf  9252  infmo  9263  brttrcl2  9481  rankc1  9637  cp  9658  isinfcard  9857  aceq1  9882  aceq2  9884  dfac5lem3  9890  dfac10b  9904  dfac12a  9913  dffin7-2  10163  dfacfin7  10164  fin1a2lem6  10170  iunfo  10304  konigthlem  10333  axgroth6  10593  axgroth3  10596  sstskm  10607  ltexprlem1  10801  gt0srpr  10843  ltpsrpr  10874  map2psrpr  10875  ltresr  10905  fimaxre3  11930  sup3  11941  supaddc  11951  supmul1  11953  elnn0z  12341  elznn0nn  12342  zmin  12693  xrnemnf  12862  xrnepnf  12863  dfrp2  13137  elioomnf  13185  elxrge0  13198  elfzuzb  13259  fzass4  13303  elfz2nn0  13356  elfzo2  13399  elfzo3  13413  lbfzo0  13436  fzind2  13514  nn0opthlem1  13991  hashgt23el  14148  cotr2g  14696  rexfiuz  15068  fsumcom2  15495  prodmo  15655  fprodcom2  15703  sinltx  15907  divalglem4  16114  divalglem10  16120  4sqlem12  16666  imasleval  17261  xpsfrnel  17282  xpscf  17285  isssc  17541  isffth2  17641  ispos2  18042  ismhm  18441  issubmndb  18453  nsgacs  18799  isgim  18887  oppgcntz  18980  f1omvdco3  19066  pmtrprfvalrn  19105  efgrelexlemb  19365  pgpfac1  19692  pgpfac  19696  issrg  19752  opprsubg  19887  opprunit  19912  isirred2  19952  opprirred  19953  drngprop  20011  opprdrng  20024  issdrg2  20075  islss  20205  islbs  20347  isdomn2  20579  unocv  20894  iunocv  20895  isbasis2g  22107  tgval2  22115  ntreq0  22237  isclo2  22248  cmpcov2  22550  is1stc2  22602  1stcelcls  22621  llyi  22634  unisngl  22687  txuni2  22725  xkobval  22746  hausdiag  22805  isfbas2  22995  elfg  23031  fbasrn  23044  fmfnfmlem3  23116  isfcls  23169  alexsubALTlem2  23208  istmd  23234  istgp  23237  istrg  23324  istdrg  23326  istdrg2  23338  isms2  23612  metuel2  23730  restmetu  23735  isngp  23761  isngp2  23762  isngp3  23763  elii1  24107  isncvsngp  24322  iscph  24343  isbn  24511  pmltpc  24623  ovolfcl  24639  finiunmbl  24717  iundisj  24721  dyaddisj  24769  vitalilem1  24781  ellimc3  25052  ig1pval3  25348  plyun0  25367  plydivex  25466  aannenlem2  25498  ellogrn  25724  atandm  26035  atandm3  26037  atans2  26090  tgjustf  26843  colinearalg  27287  axeuclid  27340  nbgrsym  27739  upgrtrls  28078  upgristrl  28079  usgr2pth0  28142  iswwlks  28210  isclwwlk  28357  clwwlkneq0  28402  h2hlm  29351  issh  29579  chcon2i  29835  chcon1i  29836  chcon3i  29837  chnlei  29856  cmcm2i  29964  cmcm3i  29965  3oalem3  30035  pjdifnormii  30054  pjneli  30094  dfadj2  30256  cnvadj  30263  hhcno  30275  hhcnf  30276  eleigvec  30328  eleigvec2  30329  pjimai  30547  isst  30584  ishst  30585  cvnbtwn4  30660  chrelat4i  30744  2reucom  30837  reuxfrdf  30848  difrab2  30854  inpr0  30889  iunin1f  30906  disjnf  30918  cbvdisjf  30919  disjorf  30927  iundisjf  30937  disjexc  30941  xrdifh  31110  iundisjfi  31126  hashxpe  31136  pmtrprfv2  31366  xrnarchi  31447  isorng  31507  prmidl0  31635  ccfldextdgrr  31751  cmpcref  31809  ordtconnlem1  31883  isrrext  31959  cntnevol  32205  ddemeas  32213  omssubaddlem  32275  omssubadd  32276  eulerpartleme  32339  eulerpartlemv  32340  eulerpartlemt0  32345  eulerpartlemgvv  32352  eulerpartlemn  32357  ballotlem2  32464  ballotlemodife  32473  oddprm2  32644  bnj257  32695  bnj268  32697  bnj290  32698  bnj312  32700  bnj89  32709  bnj887  32754  bnj976  32766  bnj1019  32768  bnj1146  32780  bnj1385  32821  bnj110  32847  bnj121  32859  bnj130  32863  bnj153  32869  bnj543  32882  bnj580  32902  bnj607  32905  bnj849  32914  bnj882  32915  bnj916  32922  bnj985v  32942  bnj985  32943  bnj1033  32958  bnj1083  32967  bnj1090  32968  bnj1128  32979  bnj1174  32992  bnj1228  33000  erdszelem1  33162  cvmliftlem15  33269  snmlval  33302  satfvsuclem2  33331  satfdm  33340  elmpst  33507  mpstrcl  33512  untuni  33659  dfso3  33673  reurab  33683  xpab  33686  ot2elxp  33688  otthne  33691  dftr6  33727  coep  33728  coepr  33729  dffr5  33730  dfso2  33731  cnvco1  33735  cnvco2  33736  eldm3  33737  dfdm5  33756  dfrn5  33757  imaindm  33762  elno3  33867  conway  34002  eqscut2  34009  madeval2  34046  brsset  34200  idsset  34201  dfon3  34203  dfbigcup2  34210  dfom5b  34223  dffun10  34225  dfiota3  34234  fnimage  34240  brdomain  34244  brrange  34245  brimg  34248  brapply  34249  brcup  34250  brcap  34251  brsuccf  34252  funpartlem  34253  brrestrict  34260  dfrecs2  34261  brub  34265  altopelaltxp  34287  trer  34514  filnetlem4  34579  df3nandALT1  34597  imnand2  34600  bj-dfbi5  34764  bj-bixor  34782  bj-nnfnt  34931  bj-sbnf  35033  bj-csbsnlem  35097  bj-rcleqf  35224  bj-sscon  35228  bj-pw0ALT  35231  bj-restpw  35272  bj-opelidb1  35333  bj-imdiridlem  35365  bj-imdirco  35370  wl-df3xor2  35649  wl-3xorrot  35657  wl-3xorcoma  35658  wl-3xornot  35661  wl-df2-3mintru2  35665  wl-df3-3mintru2  35666  wl-df4-3mintru2  35667  wl-equsalvw  35706  iundif1  35760  poimirlem25  35811  poimirlem26  35812  poimirlem30  35816  ismblfin  35827  mbfposadd  35833  itg2addnclem2  35838  ftc1anc  35867  inixp  35895  prdstotbnd  35961  heibor1lem  35976  isrngohom  36132  isidl  36181  isfldidl2  36236  isdmn3  36241  sbccom2lem  36291  triantru3  36389  vvdifopab  36407  brres2  36415  eldmqsres  36429  inxpss  36454  n0el2  36475  trcoss2  36609  dfeqvrel2  36710  dfeqvrel3  36711  redundeq1  36749  redundpbi1  36751  refrelredund4  36755  funALTVfun  36816  dfeldisj3  36837  dfeldisj5  36839  pmapglbx  37790  lhpexle3  38033  cdleme25cv  38379  dicelval3  39201  diclspsn  39215  lcfls1c  39557  sn-axrep5v  40192  sn-iotalem  40196  psspwb  40210  moxfr  40521  fphpd  40645  ifpim1  41083  ifpnot  41084  ifpid2  41085  ifpim2  41086  ifpxorcor  41090  ifpnot23  41092  ifpananb  41120  ifpnannanb  41121  ifpxorxorb  41125  rp-fakeinunass  41129  snen1g  41138  pren2  41167  alephiso2  41172  undmrnresiss  41219  cnvssco  41221  cotrintab  41229  cnviun  41265  imaiun1  41266  coiun1  41267  elintima  41268  frege133d  41380  frege54cor0a  41478  or3or  41638  andi3or  41639  ntrneik4w  41717  k0004lem1  41764  ismnuprim  41919  ismnushort  41926  undisjrab  41931  nzss  41942  pm10.541  41992  compab  42067  onfrALTlem5  42169  onfrALTlem5VD  42512  inn0f  42628  eluni2f  42660  euabsneu  44533  aiotaexb  44592  aiotavb  44593  r19.32  44601  3an4ancom24  44772  ichn  44919  ichcom  44922  ichbi12i  44923  prproropf1olem0  44965  pairreueq  44973  issubmgm  45354  sgrp2sgrp  45433  islindeps  45805  elbigo  45908  reutruALT  46163  isthincd2  46330  setrec1lem3  46406  elpg  46430