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  342  pm4.71  557  pm5.32ri  575  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  1488  xorcomOLD  1507  xorass  1508  xorbi12iOLD  1518  anxordi  1520  norcomOLD  1525  nornotOLD  1527  norass  1535  hadbi  1600  hadcoma  1601  hadcomaOLD  1602  hadcomb  1603  hadnot  1605  cador  1611  cadan  1612  cadcoma  1615  cadnot  1618  nic-axALT  1678  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  2100  sbal  2161  excom  2164  19.32  2229  19.31  2230  19.42  2232  equsalv  2262  sbex  2281  sbor  2307  sbbi  2308  cbvex2v  2344  eeeanv  2350  sbnf2  2356  sbievg  2361  cbvex2  2412  equsal  2417  dfsb3  2498  mo4  2566  eu6  2574  eubii  2585  dfeu  2595  sb8eulem  2598  sb8mo  2601  cbvmovw  2602  cbvmow  2603  cbvmowOLD  2604  cbveuvw  2606  cbveuw  2607  cbveuALT  2610  eu1  2612  sbmo  2616  cbvabv  2812  cbvabw  2813  cbvabwOLD  2814  cbvab  2815  abeq1  2872  nfceqi  2903  sbabelOLD  2941  ralbii2  3088  r19.21v  3100  r2allem  3123  ralcom4OLD  3162  rexbii2  3175  reuanid  3256  rmoanid  3257  r19.32v  3267  r19.41v  3273  r19.41  3274  r19.42v  3276  r19.43  3277  ralcom  3280  ralcomf  3282  rexcomf  3283  reeanlem  3290  3reeanv  3293  2ralorOLD  3295  rabid2  3307  rabid2f  3308  rabbi  3309  reubiia  3316  rmobiia  3321  moel  3349  reu5  3351  rmo5  3355  cbvralfw  3358  cbvralfwOLD  3359  cbvrexfw  3360  cbvralf  3361  cbvrexf  3362  cbvreuw  3365  cbvrmow  3366  cbvrmowOLD  3367  cbvreu  3370  cbvrmo  3371  cbvralvw  3372  cbvrexvw  3373  cbvrmovw  3374  cbvreuvw  3375  abv  3433  abvALT  3434  cgsex4g  3466  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  eueq  3638  reu2  3655  reu6  3656  reu3  3657  rmo4  3660  rmo3f  3664  2reu5  3688  cbvsbcw  3745  cbvsbcvw  3746  cbvsbc  3747  sbccomlem  3799  rmo3  3818  rmoanim  3823  rmoanimALT  3824  cbvralcsf  3873  cbvrexcsf  3874  cbvreucsf  3875  dfss2  3903  eqss  3932  uniiunlem  4015  sspsstri  4033  compleq  4078  ssequn1  4110  unss  4114  rexun  4120  ralunb  4121  elin3  4130  incomOLD  4132  inass  4150  ssin  4161  elsymdif  4178  nssinpss  4187  dfun2  4190  difin  4192  indi  4204  indifdi  4214  indifdirOLD  4216  ssdif0  4294  inssdif0  4300  abn0  4311  rabeq0w  4314  rabeq0  4315  disj  4378  disj3  4384  ssundif  4415  ralidmw  4435  dfif2  4458  eldifpr  4590  rexsns  4602  snprc  4650  reusn  4660  difsnpss  4737  tpss  4765  dfopif  4797  pwpr  4830  eluni2  4840  elunirab  4852  uniun  4861  unissb  4870  elintrab  4888  ssintrab  4899  intun  4908  intprOLD  4911  iuncom  4928  iuncom4  4929  iunab  4977  ssiinf  4980  iunn0  4992  iinab  4993  iunin2  4996  iinun2  4998  iundif2  4999  iunun  5018  iunxun  5019  iunxiun  5022  sspwuni  5025  iinpw  5031  cbvdisj  5045  disjor  5050  brun  5121  brin  5122  brdif  5123  dftr2  5189  intexrab  5259  inuni  5262  ssext  5364  pweqb  5366  otth2  5392  propeqop  5415  vopelopabsb  5435  eqopab2bw  5454  eqopab2b  5458  pwin  5474  pwun  5478  dffr6  5538  elxp2  5604  xpiundi  5648  xpiundir  5649  poinxp  5658  soinxp  5659  frinxp  5660  seinxp  5661  weinxp  5662  inopab  5728  difopab  5729  raliunxp  5737  rexiunxp  5738  rexxpf  5745  iunxpf  5746  cnvco  5783  dmiun  5811  dmuni  5812  dm0rn0  5823  dmres  5902  restidsing  5951  cnvsym  6008  asymref  6010  codir  6014  qfto  6015  cnvopab  6031  cnvdif  6036  rniun  6040  dminss  6045  imainss  6046  difxp  6056  xpdifid  6060  dmsnn0  6099  cnvcnvsn  6111  cnvresima  6122  resco  6143  imaco  6144  rnco  6145  coiun  6149  coass  6158  ressn  6177  cnviin  6178  cnvpo  6179  cnvso  6180  xpco  6181  opreu2reurex  6186  dfpo2  6188  dflim2  6307  unisuc  6327  funcnv  6487  funcnv3  6488  fncnv  6491  fun11  6492  imadif  6502  fnres  6543  dfmpt3  6551  mptfnf  6552  fnopabg  6554  fint  6637  fin  6638  fores  6682  dff1o3  6706  f1ompt  6967  fsn  6989  imaiun  7100  isocnv2  7182  isocnv3  7183  isores2  7184  isomin  7188  eqoprab2bw  7323  eqoprab2b  7324  elpwpwel  7595  sucexb  7631  sucelon  7639  dflim4  7670  fiun  7759  f1iun  7760  f11o  7763  opabex3d  7781  opabex3rd  7782  opabex3  7783  dfopab2  7865  dfoprab3s  7866  fmpox  7880  fparlem1  7923  fparlem2  7924  fsplitOLD  7929  suppvalbr  7952  tpostpos  8033  frrlem9  8081  wfrlem8OLD  8118  wfrfunOLD  8121  dfsmo2  8149  brwitnlem  8299  oarec  8355  qsid  8530  uniinqs  8544  mapval2  8618  mapsncnv  8639  elixp2  8647  ixpin  8669  brsdom  8718  brdom2  8725  xpassen  8806  brsdom2  8837  dif1en  8907  unfilem1  9008  fiint  9021  dfsup2  9133  supmo  9141  eqinf  9173  infmo  9184  rankc1  9559  cp  9580  isinfcard  9779  aceq1  9804  aceq2  9806  dfac5lem3  9812  dfac10b  9826  dfac12a  9835  dffin7-2  10085  dfacfin7  10086  fin1a2lem6  10092  iunfo  10226  konigthlem  10255  axgroth6  10515  axgroth3  10518  sstskm  10529  ltexprlem1  10723  gt0srpr  10765  ltpsrpr  10796  map2psrpr  10797  ltresr  10827  fimaxre3  11851  sup3  11862  supaddc  11872  supmul1  11874  elnn0z  12262  elznn0nn  12263  zmin  12613  xrnemnf  12782  xrnepnf  12783  dfrp2  13057  elioomnf  13105  elxrge0  13118  elfzuzb  13179  fzass4  13223  elfz2nn0  13276  elfzo2  13319  elfzo3  13332  lbfzo0  13355  fzind2  13433  nn0opthlem1  13910  hashgt23el  14067  cotr2g  14615  rexfiuz  14987  fsumcom2  15414  prodmo  15574  fprodcom2  15622  sinltx  15826  divalglem4  16033  divalglem10  16039  4sqlem12  16585  imasleval  17169  xpsfrnel  17190  xpscf  17193  isssc  17449  isffth2  17548  ispos2  17948  ismhm  18347  issubmndb  18359  nsgacs  18705  isgim  18793  oppgcntz  18886  f1omvdco3  18972  pmtrprfvalrn  19011  efgrelexlemb  19271  pgpfac1  19598  pgpfac  19602  issrg  19658  opprsubg  19793  opprunit  19818  isirred2  19858  opprirred  19859  drngprop  19917  opprdrng  19930  issdrg2  19981  islss  20111  islbs  20253  isdomn2  20483  unocv  20797  iunocv  20798  isbasis2g  22006  tgval2  22014  ntreq0  22136  isclo2  22147  cmpcov2  22449  is1stc2  22501  1stcelcls  22520  llyi  22533  unisngl  22586  txuni2  22624  xkobval  22645  hausdiag  22704  isfbas2  22894  elfg  22930  fbasrn  22943  fmfnfmlem3  23015  isfcls  23068  alexsubALTlem2  23107  istmd  23133  istgp  23136  istrg  23223  istdrg  23225  istdrg2  23237  isms2  23511  metuel2  23627  restmetu  23632  isngp  23658  isngp2  23659  isngp3  23660  elii1  24004  isncvsngp  24218  iscph  24239  isbn  24407  pmltpc  24519  ovolfcl  24535  finiunmbl  24613  iundisj  24617  dyaddisj  24665  vitalilem1  24677  ellimc3  24948  ig1pval3  25244  plyun0  25263  plydivex  25362  aannenlem2  25394  ellogrn  25620  atandm  25931  atandm3  25933  atans2  25986  tgjustf  26738  colinearalg  27181  axeuclid  27234  nbgrsym  27633  upgrtrls  27971  upgristrl  27972  usgr2pth0  28034  iswwlks  28102  isclwwlk  28249  clwwlkneq0  28294  h2hlm  29243  issh  29471  chcon2i  29727  chcon1i  29728  chcon3i  29729  chnlei  29748  cmcm2i  29856  cmcm3i  29857  3oalem3  29927  pjdifnormii  29946  pjneli  29986  dfadj2  30148  cnvadj  30155  hhcno  30167  hhcnf  30168  eleigvec  30220  eleigvec2  30221  pjimai  30439  isst  30476  ishst  30477  cvnbtwn4  30552  chrelat4i  30636  2reucom  30729  reuxfrdf  30740  difrab2  30746  inpr0  30781  iunin1f  30798  disjnf  30810  cbvdisjf  30811  disjorf  30819  iundisjf  30829  disjexc  30833  xrdifh  31003  iundisjfi  31019  hashxpe  31029  pmtrprfv2  31259  xrnarchi  31340  isorng  31400  prmidl0  31528  ccfldextdgrr  31644  cmpcref  31702  ordtconnlem1  31776  isrrext  31850  cntnevol  32096  ddemeas  32104  omssubaddlem  32166  omssubadd  32167  eulerpartleme  32230  eulerpartlemv  32231  eulerpartlemt0  32236  eulerpartlemgvv  32243  eulerpartlemn  32248  ballotlem2  32355  ballotlemodife  32364  oddprm2  32535  bnj257  32586  bnj268  32588  bnj290  32589  bnj312  32591  bnj89  32600  bnj887  32645  bnj976  32657  bnj1019  32659  bnj1146  32671  bnj1385  32712  bnj110  32738  bnj121  32750  bnj130  32754  bnj153  32760  bnj543  32773  bnj580  32793  bnj607  32796  bnj849  32805  bnj882  32806  bnj916  32813  bnj985v  32833  bnj985  32834  bnj1033  32849  bnj1083  32858  bnj1090  32859  bnj1128  32870  bnj1174  32883  bnj1228  32891  erdszelem1  33053  cvmliftlem15  33160  snmlval  33193  satfvsuclem2  33222  satfdm  33231  elmpst  33398  mpstrcl  33403  untuni  33550  dfso3  33566  reurab  33576  xpab  33579  ot2elxp  33582  otthne  33585  dftr6  33624  coep  33625  coepr  33626  dffr5  33627  dfso2  33628  cnvco1  33632  cnvco2  33633  eldm3  33634  dfdm5  33653  dfrn5  33654  imaindm  33659  brttrcl2  33700  elno3  33785  conway  33920  eqscut2  33927  madeval2  33964  brsset  34118  idsset  34119  dfon3  34121  dfbigcup2  34128  dfom5b  34141  dffun10  34143  dfiota3  34152  fnimage  34158  brdomain  34162  brrange  34163  brimg  34166  brapply  34167  brcup  34168  brcap  34169  brsuccf  34170  funpartlem  34171  brrestrict  34178  dfrecs2  34179  brub  34183  altopelaltxp  34205  trer  34432  filnetlem4  34497  df3nandALT1  34515  imnand2  34518  bj-dfbi5  34682  bj-bixor  34700  bj-nnfnt  34849  bj-sbnf  34951  bj-csbsnlem  35015  bj-rcleqf  35142  bj-sscon  35146  bj-pw0ALT  35149  bj-restpw  35190  bj-opelidb1  35251  bj-imdiridlem  35283  bj-imdirco  35288  wl-df3xor2  35567  wl-3xorrot  35575  wl-3xorcoma  35576  wl-3xornot  35579  wl-df2-3mintru2  35583  wl-df3-3mintru2  35584  wl-df4-3mintru2  35585  wl-equsalvw  35624  iundif1  35678  poimirlem25  35729  poimirlem26  35730  poimirlem30  35734  ismblfin  35745  mbfposadd  35751  itg2addnclem2  35756  ftc1anc  35785  inixp  35813  prdstotbnd  35879  heibor1lem  35894  isrngohom  36050  isidl  36099  isfldidl2  36154  isdmn3  36159  sbccom2lem  36209  triantru3  36307  vvdifopab  36326  brres2  36334  eldmqsres  36348  inxpss  36374  n0el2  36395  trcoss2  36529  dfeqvrel2  36630  dfeqvrel3  36631  redundeq1  36669  redundpbi1  36671  refrelredund4  36675  funALTVfun  36736  dfeldisj3  36757  dfeldisj5  36759  pmapglbx  37710  lhpexle3  37953  cdleme25cv  38299  dicelval3  39121  diclspsn  39135  lcfls1c  39477  sn-axrep5v  40113  sn-iotalem  40117  psspwb  40129  moxfr  40430  fphpd  40554  ifpim1  40974  ifpnot  40975  ifpid2  40976  ifpim2  40977  ifpxorcor  40981  ifpnot23  40983  ifpananb  41011  ifpnannanb  41012  ifpxorxorb  41016  rp-fakeinunass  41020  snen1g  41029  pren2  41049  alephiso2  41054  undmrnresiss  41101  cnvssco  41103  cotrintab  41111  cnviun  41147  imaiun1  41148  coiun1  41149  elintima  41150  frege133d  41262  frege54cor0a  41360  or3or  41520  andi3or  41521  ntrneik4w  41599  k0004lem1  41646  ismnuprim  41801  ismnushort  41808  undisjrab  41813  nzss  41824  pm10.541  41874  compab  41949  onfrALTlem5  42051  onfrALTlem5VD  42394  inn0f  42510  eluni2f  42542  euabsneu  44409  aiotaexb  44468  aiotavb  44469  r19.32  44477  3an4ancom24  44648  ichn  44796  ichcom  44799  ichbi12i  44800  prproropf1olem0  44842  pairreueq  44850  issubmgm  45231  sgrp2sgrp  45310  islindeps  45682  elbigo  45785  reutruALT  46040  isthincd2  46207  setrec1lem3  46281  elpg  46305