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 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  559  pm5.32ri  577  an31  647  pm4.14  806  or4  926  orimdi  930  orbidi  952  ordi  1005  ordir  1006  andir  1008  dfbi3  1049  dfifp7  1069  ifpdfbi  1070  ifpn  1073  ifpnOLD  1074  3orrot  1093  3orcoma  1094  3ioran  1107  3ianor  1108  3anbi123i  1156  3orbi123i  1157  an6  1446  3or6  1448  an33rean  1484  an33reanOLD  1485  nancom  1495  xorcomOLD  1514  xorass  1515  xorbi12iOLD  1525  anxordi  1527  norcomOLD  1532  norass  1539  hadbi  1600  hadcoma  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  2259  sbex  2278  sbrim  2301  sbor  2304  sbbi  2305  cbvex2v  2341  eeeanv  2347  sbnf2  2355  cbvsbvf  2361  cbvex2  2412  equsal  2417  dfsb3  2494  mo4  2561  eu6  2569  eubii  2580  dfeu  2590  sb8eulem  2593  sb8mo  2596  cbvmovw  2597  cbvmow  2598  cbvmowOLD  2599  cbveuvw  2601  cbveuw  2602  cbveuALT  2605  eu1  2607  sbmo  2611  cbvabv  2806  cbvabw  2807  cbvabwOLD  2808  cbvab  2809  eqabcb  2876  nfceqi  2901  sbabelOLD  2940  ralbii2  3090  rexbii2  3091  r19.43  3123  r2allem  3143  r19.21vOLD  3181  r19.41v  3189  r19.42v  3191  r19.32v  3192  reeanlem  3226  3reeanv  3228  2ralorOLD  3230  cbvralvw  3235  cbvrexvw  3236  r19.41  3261  ralcom4OLD  3285  ralcom  3287  ralcomf  3300  rexcomf  3301  cbvralfw  3302  cbvralfwOLD  3321  cbvralf  3357  cbvrexf  3358  reu5  3379  rmobiia  3383  reubiia  3384  rmoanidOLD  3389  reuanidOLD  3390  rmo5  3397  cbvrmovw  3400  cbvreuvw  3401  moelOLD  3402  cbvrmow  3406  cbvreuw  3407  cbvrmowOLD  3412  cbvreuwOLD  3413  cbvreu  3425  cbvrmo  3426  rabid2f  3464  rabid2OLD  3466  abv  3486  abvALT  3487  ceqsal  3510  ceqsalv  3512  cgsex4gOLD  3522  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  reurab  3697  eueq  3704  reu2  3721  reu6  3722  reu3  3723  rmo4  3726  rmo3f  3730  2reu5  3754  cbvsbcw  3811  cbvsbcvw  3812  cbvsbc  3813  sbccomlem  3864  rmo3  3883  rmoanim  3888  rmoanimALT  3889  cbvralcsf  3938  cbvrexcsf  3939  cbvreucsf  3940  dfss2  3968  eqss  3997  uniiunlem  4084  sspsstri  4102  compleq  4147  ssequn1  4180  unss  4184  rexun  4190  ralunb  4191  elin3  4200  inass  4219  ssin  4230  elsymdif  4247  nssinpss  4256  dfun2  4259  difin  4261  indi  4273  indifdi  4283  indifdirOLD  4285  ssdif0  4363  inssdif0  4369  ab0  4374  abn0  4380  rabeq0w  4383  rabeq0  4384  disj  4447  disj3  4453  ssundif  4487  ralidmw  4507  dfif2  4530  eldifpr  4660  rexsns  4673  snprc  4721  reusn  4731  difsnpss  4810  tpss  4838  pwpr  4902  eluni2  4912  elunirab  4924  uniun  4934  unissb  4943  unissbOLD  4944  elintrab  4964  ssintrab  4975  intun  4984  intprOLD  4987  iuncom  5004  iuncom4  5005  iunab  5054  ssiinf  5057  iunn0  5070  iinab  5071  iunin2  5074  iinun2  5076  iundif2  5077  iunun  5096  iunxun  5097  iunxiun  5100  sspwuni  5103  iinpw  5109  cbvdisj  5123  disjor  5128  brun  5199  brin  5200  brdif  5201  dftr2  5267  dftr5  5269  intexrab  5340  inuni  5343  ssext  5454  pweqb  5456  otth2  5483  otthne  5486  propeqop  5507  vopelopabsb  5529  eqopab2bw  5548  eqopab2b  5552  pwin  5570  pwun  5572  dffr6  5634  elxp2  5700  otelxp  5719  xpiundi  5745  xpiundir  5746  poinxp  5755  soinxp  5756  frinxp  5757  seinxp  5758  weinxp  5759  inopab  5828  difopab  5829  difopabOLD  5830  raliunxp  5838  rexiunxp  5839  rexxpf  5846  iunxpf  5847  cnvco  5884  dmiun  5912  dmuni  5913  dm0rn0  5923  dmres  6002  restidsing  6051  cnvsymOLDOLD  6113  asymref  6115  codir  6119  qfto  6120  cnvopab  6136  cnvdif  6141  rniun  6145  dminss  6150  imainss  6151  difxp  6161  xpdifid  6165  dmsnn0  6204  cnvcnvsn  6216  cnvresima  6227  resco  6247  imaco  6248  rnco  6249  coiun  6253  coass  6262  ressn  6282  cnviin  6283  cnvpo  6284  cnvso  6285  xpco  6286  opreu2reurex  6291  dfpo2  6293  imaindm  6296  dflim2  6419  funcnv  6615  funcnv3  6616  fncnv  6619  fun11  6620  imadif  6630  fnres  6675  dfmpt3  6682  mptfnf  6683  fnopabg  6685  fint  6768  fin  6769  fores  6813  dff1o3  6837  f1ompt  7108  fsn  7130  imaiun  7241  isocnv2  7325  isocnv3  7326  isores2  7327  isomin  7331  eqoprab2bw  7476  eqoprab2b  7477  elpwpwel  7751  sucexb  7789  onsucb  7802  dflim4  7834  fiun  7926  f1iun  7927  f11o  7930  opabex3d  7949  opabex3rd  7950  opabex3  7951  dfopab2  8035  dfoprab3s  8036  fmpox  8050  fparlem1  8095  fparlem2  8096  tpostpos  8228  frrlem9  8276  wfrlem8OLD  8313  wfrfunOLD  8316  dfsmo2  8344  brwitnlem  8504  oarec  8559  naddasslem1  8690  naddasslem2  8691  qsid  8774  uniinqs  8788  mapval2  8863  mapsncnv  8884  elixp2  8892  ixpin  8914  brsdom  8968  brdom2  8975  xpassen  9063  brsdom2  9094  dif1enOLD  9159  unfilem1  9307  fiint  9321  dfsup2  9436  supmo  9444  eqinf  9476  infmo  9487  brttrcl2  9706  rankc1  9862  cp  9883  isinfcard  10084  aceq1  10109  aceq2  10111  dfac5lem3  10117  dfac10b  10131  dfac12a  10140  dffin7-2  10390  dfacfin7  10391  fin1a2lem6  10397  iunfo  10531  konigthlem  10560  axgroth6  10820  axgroth3  10823  sstskm  10834  ltexprlem1  11028  gt0srpr  11070  ltpsrpr  11101  map2psrpr  11102  ltresr  11132  fimaxre3  12157  sup3  12168  supaddc  12178  supmul1  12180  elnn0z  12568  elznn0nn  12569  zmin  12925  xrnemnf  13094  xrnepnf  13095  dfrp2  13370  elioomnf  13418  elxrge0  13431  elfzuzb  13492  fzass4  13536  elfz2nn0  13589  elfzo2  13632  elfzo3  13646  lbfzo0  13669  fzind2  13747  nn0opthlem1  14225  hashgt23el  14381  cotr2g  14920  rexfiuz  15291  fsumcom2  15717  prodmo  15877  fprodcom2  15925  sinltx  16129  divalglem4  16336  divalglem10  16342  4sqlem12  16886  imasleval  17484  xpsfrnel  17505  xpscf  17508  isssc  17764  isffth2  17864  ispos2  18265  ismhm  18670  issubmndb  18683  nsgacs  19037  isgim  19131  oppgcntz  19226  f1omvdco3  19312  pmtrprfvalrn  19351  efgrelexlemb  19613  pgpfac1  19945  pgpfac  19949  issrg  20005  opprsubg  20159  opprunit  20184  isirred2  20228  opprirred  20229  drngprop  20323  opprdrng  20340  issdrg2  20404  islss  20538  islbs  20680  isdomn2  20908  unocv  21225  iunocv  21226  isbasis2g  22443  tgval2  22451  ntreq0  22573  isclo2  22584  cmpcov2  22886  is1stc2  22938  1stcelcls  22957  llyi  22970  unisngl  23023  txuni2  23061  xkobval  23082  hausdiag  23141  isfbas2  23331  elfg  23367  fbasrn  23380  fmfnfmlem3  23452  isfcls  23505  alexsubALTlem2  23544  istmd  23570  istgp  23573  istrg  23660  istdrg  23662  istdrg2  23674  isms2  23948  metuel2  24066  restmetu  24071  isngp  24097  isngp2  24098  isngp3  24099  elii1  24443  isncvsngp  24658  iscph  24679  isbn  24847  pmltpc  24959  ovolfcl  24975  finiunmbl  25053  iundisj  25057  dyaddisj  25105  vitalilem1  25117  ellimc3  25388  ig1pval3  25684  plyun0  25703  plydivex  25802  aannenlem2  25834  ellogrn  26060  atandm  26371  atandm3  26373  atans2  26426  elno3  27148  conway  27290  eqscut2  27297  madeval2  27338  tgjustf  27714  colinearalg  28158  axeuclid  28211  nbgrsym  28610  upgrtrls  28948  upgristrl  28949  usgr2pth0  29012  iswwlks  29080  isclwwlk  29227  clwwlkneq0  29272  h2hlm  30221  issh  30449  chcon2i  30705  chcon1i  30706  chcon3i  30707  chnlei  30726  cmcm2i  30834  cmcm3i  30835  3oalem3  30905  pjdifnormii  30924  pjneli  30964  dfadj2  31126  cnvadj  31133  hhcno  31145  hhcnf  31146  eleigvec  31198  eleigvec2  31199  pjimai  31417  isst  31454  ishst  31455  cvnbtwn4  31530  chrelat4i  31614  2reucom  31708  reuxfrdf  31719  difrab2  31726  inpr0  31757  iunin1f  31777  disjnf  31789  cbvdisjf  31790  disjorf  31798  iundisjf  31808  disjexc  31812  xrdifh  31979  iundisjfi  31995  hashxpe  32007  pmtrprfv2  32237  xrnarchi  32318  isorng  32406  prmidl0  32558  opprnsg  32587  ccfldextdgrr  32735  cmpcref  32819  ordtconnlem1  32893  isrrext  32969  cntnevol  33215  ddemeas  33223  omssubaddlem  33287  omssubadd  33288  eulerpartleme  33351  eulerpartlemv  33352  eulerpartlemt0  33357  eulerpartlemgvv  33364  eulerpartlemn  33369  ballotlem2  33476  ballotlemodife  33485  oddprm2  33656  bnj257  33707  bnj268  33709  bnj290  33710  bnj312  33712  bnj89  33721  bnj887  33765  bnj976  33777  bnj1019  33779  bnj1146  33791  bnj1385  33832  bnj110  33858  bnj121  33870  bnj130  33874  bnj153  33880  bnj543  33893  bnj580  33913  bnj607  33916  bnj849  33925  bnj882  33926  bnj916  33933  bnj985v  33953  bnj985  33954  bnj1033  33969  bnj1083  33978  bnj1090  33979  bnj1128  33990  bnj1174  34003  bnj1228  34011  erdszelem1  34171  cvmliftlem15  34278  snmlval  34311  satfvsuclem2  34340  satfdm  34349  elmpst  34516  mpstrcl  34521  untuni  34667  dfso3  34678  xpab  34684  dftr6  34710  coep  34711  coepr  34712  dffr5  34713  dfso2  34714  cnvco1  34718  cnvco2  34719  eldm3  34720  dfdm5  34733  dfrn5  34734  brsset  34850  idsset  34851  dfon3  34853  dfbigcup2  34860  dfom5b  34873  dffun10  34875  dfiota3  34884  fnimage  34890  brdomain  34894  brrange  34895  brimg  34898  brapply  34899  brcup  34900  brcap  34901  brsuccf  34902  funpartlem  34903  brrestrict  34910  dfrecs2  34911  brub  34915  altopelaltxp  34937  trer  35190  filnetlem4  35255  df3nandALT1  35273  imnand2  35276  bj-dfbi5  35440  bj-bixor  35458  bj-nnfnt  35607  bj-sbnf  35708  bj-csbsnlem  35772  bj-rcleqf  35895  bj-sscon  35899  bj-pw0ALT  35919  bj-restpw  35962  bj-opelidb1  36023  bj-imdiridlem  36055  bj-imdirco  36060  wl-df3xor2  36339  wl-3xorrot  36347  wl-3xorcoma  36348  wl-3xornot  36351  wl-df2-3mintru2  36355  wl-df3-3mintru2  36356  wl-df4-3mintru2  36357  wl-equsalvw  36396  iundif1  36451  poimirlem25  36502  poimirlem26  36503  poimirlem30  36507  ismblfin  36518  mbfposadd  36524  itg2addnclem2  36529  ftc1anc  36558  inixp  36585  prdstotbnd  36651  heibor1lem  36666  isrngohom  36822  isidl  36871  isfldidl2  36926  isdmn3  36931  sbccom2lem  36981  triantru3  37083  vvdifopab  37117  brres2  37125  eldmqsres  37144  inxpss  37169  ref5  37171  n0el2  37191  trcoss2  37343  dfeqvrel2  37449  dfeqvrel3  37450  redundeq1  37488  redundpbi1  37490  refrelredund4  37494  funALTVfun  37557  dfeldisj3  37578  dfeldisj5  37580  pet0  37674  petid  37676  petidres  37678  petinidres  37680  petxrnidres  37682  mpet  37698  petincnvepres  37708  pet  37710  pmapglbx  38629  lhpexle3  38872  cdleme25cv  39218  dicelval3  40040  diclspsn  40054  lcfls1c  40396  sn-axrep5v  41030  sn-iotalem  41035  psspwb  41043  moxfr  41416  fphpd  41540  uniel  41952  dflim6  42000  onsucf1olem  42006  dflim7  42009  omge2  42034  oenassex  42054  safesnsupfilb  42155  ifpim1  42206  ifpnot  42207  ifpid2  42208  ifpim2  42209  ifpxorcor  42213  ifpnot23  42215  ifpananb  42243  ifpnannanb  42244  ifpxorxorb  42248  rp-fakeinunass  42252  snen1g  42261  pren2  42290  alephiso2  42295  undmrnresiss  42341  cnvssco  42343  cotrintab  42351  cnviun  42387  imaiun1  42388  coiun1  42389  elintima  42390  frege133d  42502  frege54cor0a  42600  or3or  42760  andi3or  42761  ntrneik4w  42837  k0004lem1  42884  ismnuprim  43039  ismnushort  43046  undisjrab  43051  nzss  43062  pm10.541  43112  compab  43187  onfrALTlem5  43289  onfrALTlem5VD  43632  inn0f  43746  eluni2f  43778  euabsneu  45725  aiotaexb  45784  aiotavb  45785  r19.32  45793  3an4ancom24  45964  ichn  46111  ichcom  46114  ichbi12i  46115  prproropf1olem0  46157  pairreueq  46165  issubmgm  46546  sgrp2sgrp  46625  islindeps  47088  elbigo  47191  reutruALT  47445  isthincd2  47612  setrec1lem3  47688  elpg  47713