Theorem 3bitr4i 302

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  341  pm4.71  556  pm5.32ri  574  an31  644  pm4.14  803  or4  923  orimdi  927  orbidi  949  ordi  1002  ordir  1003  andir  1005  dfbi3  1046  dfifp7  1066  ifpdfbi  1067  ifpn  1070  ifpnOLD  1071  3orrot  1090  3orcoma  1091  3ioran  1104  3ianor  1105  3anbi123i  1153  3orbi123i  1154  an6  1443  3or6  1445  an33rean  1481  an33reanOLD  1482  nancom  1492  xorcomOLD  1511  xorass  1512  xorbi12iOLD  1522  anxordi  1524  norcomOLD  1529  norass  1536  hadbi  1597  hadcoma  1598  hadcomb  1599  hadnot  1601  cador  1607  cadan  1608  cadcoma  1611  cadnot  1614  nic-axALT  1674  nfnbiOLD  1856  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1955  4exdistr  1963  cbvexvw  2038  exexw  2052  sb3an  2082  sbcom4  2090  sbcom3vv  2096  sbal  2157  excom  2160  19.32  2224  19.31  2225  19.42  2227  equsalv  2256  sbex  2275  sbrim  2298  sbor  2301  sbbi  2302  cbvex2v  2338  eeeanv  2344  sbnf2  2352  cbvsbvf  2358  cbvex2  2409  equsal  2414  dfsb3  2491  mo4  2558  eu6  2566  eubii  2577  dfeu  2587  sb8eulem  2590  sb8mo  2593  cbvmovw  2594  cbvmow  2595  cbvmowOLD  2596  cbveuvw  2598  cbveuw  2599  cbveuALT  2602  eu1  2604  sbmo  2608  cbvabv  2803  cbvabw  2804  cbvabwOLD  2805  cbvab  2806  eqabcb  2873  nfceqi  2898  sbabelOLD  2937  ralbii2  3087  rexbii2  3088  r19.43  3120  r2allem  3140  r19.21vOLD  3178  r19.41v  3186  r19.42v  3188  r19.32v  3189  reeanlem  3223  3reeanv  3225  2ralorOLD  3227  cbvralvw  3232  cbvrexvw  3233  r19.41  3258  ralcom4OLD  3282  ralcom  3284  ralcomf  3297  rexcomf  3298  cbvralfw  3299  cbvralfwOLD  3318  cbvralf  3354  cbvrexf  3355  reu5  3376  rmobiia  3380  reubiia  3381  rmoanidOLD  3386  reuanidOLD  3387  rmo5  3394  cbvrmovw  3397  cbvreuvw  3398  moelOLD  3399  cbvrmow  3403  cbvreuw  3404  cbvrmowOLD  3409  cbvreuwOLD  3410  cbvreu  3422  cbvrmo  3423  rabid2f  3461  rabid2OLD  3463  abv  3483  abvALT  3484  ceqsal  3508  ceqsalv  3510  cgsex4gOLD  3520  ceqsex3v  3530  ceqsex4v  3531  ceqsex8v  3533  reurab  3696  eueq  3703  reu2  3720  reu6  3721  reu3  3722  rmo4  3725  rmo3f  3729  2reu5  3753  cbvsbcw  3810  cbvsbcvw  3811  cbvsbc  3812  sbccomlem  3863  rmo3  3882  rmoanim  3887  rmoanimALT  3888  cbvralcsf  3937  cbvrexcsf  3938  cbvreucsf  3939  dfss2  3967  eqss  3996  uniiunlem  4083  sspsstri  4101  compleq  4146  ssequn1  4179  unss  4183  rexun  4189  ralunb  4190  elin3  4199  inass  4218  ssin  4229  elsymdif  4246  nssinpss  4255  dfun2  4258  difin  4260  indi  4272  indifdi  4282  indifdirOLD  4284  ssdif0  4362  inssdif0  4368  ab0  4373  abn0  4379  rabeq0w  4382  rabeq0  4383  disj  4446  disj3  4452  ssundif  4486  ralidmw  4506  dfif2  4529  eldifpr  4659  rexsns  4672  snprc  4720  reusn  4730  difsnpss  4809  tpss  4837  pwpr  4901  eluni2  4911  elunirab  4923  uniun  4933  unissb  4942  unissbOLD  4943  elintrab  4963  ssintrab  4974  intun  4983  intprOLD  4986  iuncom  5003  iuncom4  5004  iunab  5053  ssiinf  5056  iunn0  5069  iinab  5070  iunin2  5073  iinun2  5075  iundif2  5076  iunun  5095  iunxun  5096  iunxiun  5099  sspwuni  5102  iinpw  5108  cbvdisj  5122  disjor  5127  brun  5198  brin  5199  brdif  5200  dftr2  5266  dftr5  5268  intexrab  5339  inuni  5342  ssext  5453  pweqb  5455  otth2  5482  otthne  5485  propeqop  5506  vopelopabsb  5528  eqopab2bw  5547  eqopab2b  5551  pwin  5569  pwun  5571  dffr6  5633  elxp2  5699  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  6114  asymref  6116  codir  6120  qfto  6121  cnvopab  6137  cnvdif  6142  rniun  6146  dminss  6151  imainss  6152  difxp  6162  xpdifid  6166  dmsnn0  6205  cnvcnvsn  6217  cnvresima  6228  resco  6248  imaco  6249  rnco  6250  coiun  6254  coass  6263  ressn  6283  cnviin  6284  cnvpo  6285  cnvso  6286  xpco  6287  opreu2reurex  6292  dfpo2  6294  imaindm  6297  dflim2  6420  funcnv  6616  funcnv3  6617  fncnv  6620  fun11  6621  imadif  6631  fnres  6676  dfmpt3  6683  mptfnf  6684  fnopabg  6686  fint  6769  fin  6770  fores  6814  dff1o3  6838  f1ompt  7111  fsn  7134  imaiun  7246  isocnv2  7330  isocnv3  7331  isores2  7332  isomin  7336  eqoprab2bw  7481  eqoprab2b  7482  elpwpwel  7756  sucexb  7794  onsucb  7807  dflim4  7839  fiun  7931  f1iun  7932  f11o  7935  opabex3d  7954  opabex3rd  7955  opabex3  7956  dfopab2  8040  dfoprab3s  8041  fmpox  8055  fparlem1  8100  fparlem2  8101  tpostpos  8233  frrlem9  8281  wfrlem8OLD  8318  wfrfunOLD  8321  dfsmo2  8349  brwitnlem  8509  oarec  8564  naddasslem1  8695  naddasslem2  8696  qsid  8779  uniinqs  8793  mapval2  8868  mapsncnv  8889  elixp2  8897  ixpin  8919  brsdom  8973  brdom2  8980  xpassen  9068  brsdom2  9099  dif1enOLD  9164  unfilem1  9312  fiint  9326  dfsup2  9441  supmo  9449  eqinf  9481  infmo  9492  brttrcl2  9711  rankc1  9867  cp  9888  isinfcard  10089  aceq1  10114  aceq2  10116  dfac5lem3  10122  dfac10b  10136  dfac12a  10145  dffin7-2  10395  dfacfin7  10396  fin1a2lem6  10402  iunfo  10536  konigthlem  10565  axgroth6  10825  axgroth3  10828  sstskm  10839  ltexprlem1  11033  gt0srpr  11075  ltpsrpr  11106  map2psrpr  11107  ltresr  11137  fimaxre3  12164  sup3  12175  supaddc  12185  supmul1  12187  elnn0z  12575  elznn0nn  12576  zmin  12932  xrnemnf  13101  xrnepnf  13102  dfrp2  13377  elioomnf  13425  elxrge0  13438  elfzuzb  13499  fzass4  13543  elfz2nn0  13596  elfzo2  13639  elfzo3  13653  lbfzo0  13676  fzind2  13754  nn0opthlem1  14232  hashgt23el  14388  cotr2g  14927  rexfiuz  15298  fsumcom2  15724  prodmo  15884  fprodcom2  15932  sinltx  16136  divalglem4  16343  divalglem10  16349  4sqlem12  16893  imasleval  17491  xpsfrnel  17512  xpscf  17515  isssc  17771  isffth2  17871  ispos2  18272  issubmgm  18627  ismhm  18707  issubmndb  18722  nsgacs  19078  isgim  19176  oppgcntz  19272  f1omvdco3  19358  pmtrprfvalrn  19397  efgrelexlemb  19659  pgpfac1  19991  pgpfac  19995  issrg  20082  opprsubg  20243  opprunit  20268  isirred2  20312  opprirred  20313  drngprop  20515  opprdrng  20532  issdrg2  20554  islss  20689  islbs  20831  isdomn2  21115  unocv  21452  iunocv  21453  isbasis2g  22671  tgval2  22679  ntreq0  22801  isclo2  22812  cmpcov2  23114  is1stc2  23166  1stcelcls  23185  llyi  23198  unisngl  23251  txuni2  23289  xkobval  23310  hausdiag  23369  isfbas2  23559  elfg  23595  fbasrn  23608  fmfnfmlem3  23680  isfcls  23733  alexsubALTlem2  23772  istmd  23798  istgp  23801  istrg  23888  istdrg  23890  istdrg2  23902  isms2  24176  metuel2  24294  restmetu  24299  isngp  24325  isngp2  24326  isngp3  24327  elii1  24678  isncvsngp  24897  iscph  24918  isbn  25086  pmltpc  25199  ovolfcl  25215  finiunmbl  25293  iundisj  25297  dyaddisj  25345  vitalilem1  25357  ellimc3  25628  ig1pval3  25927  plyun0  25946  plydivex  26046  aannenlem2  26078  ellogrn  26304  atandm  26617  atandm3  26619  atans2  26672  elno3  27394  conway  27537  eqscut2  27544  madeval2  27585  tgjustf  27991  colinearalg  28435  axeuclid  28488  nbgrsym  28887  upgrtrls  29225  upgristrl  29226  usgr2pth0  29289  iswwlks  29357  isclwwlk  29504  clwwlkneq0  29549  h2hlm  30500  issh  30728  chcon2i  30984  chcon1i  30985  chcon3i  30986  chnlei  31005  cmcm2i  31113  cmcm3i  31114  3oalem3  31184  pjdifnormii  31203  pjneli  31243  dfadj2  31405  cnvadj  31412  hhcno  31424  hhcnf  31425  eleigvec  31477  eleigvec2  31478  pjimai  31696  isst  31733  ishst  31734  cvnbtwn4  31809  chrelat4i  31893  2reucom  31987  reuxfrdf  31998  difrab2  32005  inpr0  32036  iunin1f  32056  disjnf  32068  cbvdisjf  32069  disjorf  32077  iundisjf  32087  disjexc  32091  xrdifh  32258  iundisjfi  32274  hashxpe  32286  pmtrprfv2  32519  xrnarchi  32600  isorng  32687  prmidl0  32843  opprnsg  32872  ccfldextdgrr  33035  cmpcref  33128  ordtconnlem1  33202  isrrext  33278  cntnevol  33524  ddemeas  33532  omssubaddlem  33596  omssubadd  33597  eulerpartleme  33660  eulerpartlemv  33661  eulerpartlemt0  33666  eulerpartlemgvv  33673  eulerpartlemn  33678  ballotlem2  33785  ballotlemodife  33794  oddprm2  33965  bnj257  34016  bnj268  34018  bnj290  34019  bnj312  34021  bnj89  34030  bnj887  34074  bnj976  34086  bnj1019  34088  bnj1146  34100  bnj1385  34141  bnj110  34167  bnj121  34179  bnj130  34183  bnj153  34189  bnj543  34202  bnj580  34222  bnj607  34225  bnj849  34234  bnj882  34235  bnj916  34242  bnj985v  34262  bnj985  34263  bnj1033  34278  bnj1083  34287  bnj1090  34288  bnj1128  34299  bnj1174  34312  bnj1228  34320  erdszelem1  34480  cvmliftlem15  34587  snmlval  34620  satfvsuclem2  34649  satfdm  34658  elmpst  34825  mpstrcl  34830  untuni  34982  dfso3  34993  xpab  34999  dftr6  35025  coep  35026  coepr  35027  dffr5  35028  dfso2  35029  cnvco1  35033  cnvco2  35034  eldm3  35035  dfdm5  35048  dfrn5  35049  brsset  35165  idsset  35166  dfon3  35168  dfbigcup2  35175  dfom5b  35188  dffun10  35190  dfiota3  35199  fnimage  35205  brdomain  35209  brrange  35210  brimg  35213  brapply  35214  brcup  35215  brcap  35216  brsuccf  35217  funpartlem  35218  brrestrict  35225  dfrecs2  35226  brub  35230  altopelaltxp  35252  trer  35504  filnetlem4  35569  df3nandALT1  35587  imnand2  35590  bj-dfbi5  35754  bj-bixor  35772  bj-nnfnt  35921  bj-sbnf  36022  bj-csbsnlem  36086  bj-rcleqf  36209  bj-sscon  36213  bj-pw0ALT  36233  bj-restpw  36276  bj-opelidb1  36337  bj-imdiridlem  36369  bj-imdirco  36374  wl-df3xor2  36653  wl-3xorrot  36661  wl-3xorcoma  36662  wl-3xornot  36665  wl-df2-3mintru2  36669  wl-df3-3mintru2  36670  wl-df4-3mintru2  36671  wl-equsalvw  36710  iundif1  36765  poimirlem25  36816  poimirlem26  36817  poimirlem30  36821  ismblfin  36832  mbfposadd  36838  itg2addnclem2  36843  ftc1anc  36872  inixp  36899  prdstotbnd  36965  heibor1lem  36980  isrngohom  37136  isidl  37185  isfldidl2  37240  isdmn3  37245  sbccom2lem  37295  triantru3  37397  vvdifopab  37431  brres2  37439  eldmqsres  37458  inxpss  37483  ref5  37485  n0el2  37505  trcoss2  37657  dfeqvrel2  37763  dfeqvrel3  37764  redundeq1  37802  redundpbi1  37804  refrelredund4  37808  funALTVfun  37871  dfeldisj3  37892  dfeldisj5  37894  pet0  37988  petid  37990  petidres  37992  petinidres  37994  petxrnidres  37996  mpet  38012  petincnvepres  38022  pet  38024  pmapglbx  38943  lhpexle3  39186  cdleme25cv  39532  dicelval3  40354  diclspsn  40368  lcfls1c  40710  sn-axrep5v  41339  sn-iotalem  41344  psspwb  41352  moxfr  41732  fphpd  41856  uniel  42268  dflim6  42316  onsucf1olem  42322  dflim7  42325  omge2  42350  oenassex  42370  safesnsupfilb  42471  ifpim1  42522  ifpnot  42523  ifpid2  42524  ifpim2  42525  ifpxorcor  42529  ifpnot23  42531  ifpananb  42559  ifpnannanb  42560  ifpxorxorb  42564  rp-fakeinunass  42568  snen1g  42577  pren2  42606  alephiso2  42611  undmrnresiss  42657  cnvssco  42659  cotrintab  42667  cnviun  42703  imaiun1  42704  coiun1  42705  elintima  42706  frege133d  42818  frege54cor0a  42916  or3or  43076  andi3or  43077  ntrneik4w  43153  k0004lem1  43200  ismnuprim  43355  ismnushort  43362  undisjrab  43367  nzss  43378  pm10.541  43428  compab  43503  onfrALTlem5  43605  onfrALTlem5VD  43948  inn0f  44061  eluni2f  44093  euabsneu  46036  aiotaexb  46095  aiotavb  46096  r19.32  46104  3an4ancom24  46275  ichn  46422  ichcom  46425  ichbi12i  46426  prproropf1olem0  46468  pairreueq  46476  sgrp2sgrp  46904  islindeps  47221  elbigo  47324  reutruALT  47578  isthincd2  47745  setrec1lem3  47821  elpg  47846