Theorem 3bitr4i 305

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi2d  345  pm4.71  560  pm5.32ri  578  an31  646  pm4.14  805  or4  923  orimdi  927  orbidi  949  ordi  1002  ordir  1003  andir  1005  dfbi3  1044  dfifp7  1064  ifpn  1067  3orrot  1088  3orcoma  1089  3ioran  1102  3ianor  1103  3anbi123i  1151  3orbi123i  1152  an6  1441  3or6  1443  an33rean  1479  an33reanOLD  1480  nancom  1486  xorcomOLD  1505  xorass  1506  xorbi12iOLD  1516  anxordi  1518  norcomOLD  1523  nornotOLD  1525  norass  1533  hadbi  1598  hadcoma  1599  hadcomaOLD  1600  hadcomb  1601  hadnot  1603  cador  1609  cadan  1610  cadcoma  1613  cadnot  1616  nic-axALT  1675  nfnbi  1855  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1963  cbvexvw  2044  sbcom4  2099  sbcom3vv  2106  sbal  2166  excom  2169  19.32  2235  19.31  2236  19.42  2238  equsalv  2268  sbex  2288  sbanOLD  2312  sbor  2316  sbbi  2317  sbnvOLD  2322  sbanvOLD  2326  sbbivOLD  2327  cbvexv1  2362  cbvex2v  2365  eeeanv  2371  sbnf2  2377  cbvex2  2434  equsal  2439  dfsb3  2533  dfsb3ALT  2592  sbanALT  2610  sbbiALT  2611  mo4  2650  eu6  2659  eubii  2670  dfeu  2681  sb8eulem  2684  sb8mo  2687  cbvmow  2688  cbveuALT  2692  eu1  2694  sbmo  2698  cbvabv  2889  cbvabw  2890  cbvab  2891  abeq1  2946  nfceqi  2973  sbabel  3015  ralbii2  3163  r19.21v  3175  r2allem  3200  ralcom4  3235  rexbii2  3245  rexanidOLD  3253  reuanid  3328  rmoanid  3329  r19.30OLD  3339  r19.32v  3340  r19.41v  3347  r19.41  3348  r19.42v  3350  r19.43  3351  ralcom  3354  rexcomOLD  3356  ralcomf  3357  rexcomf  3358  reeanlem  3365  3reeanv  3368  2ralor  3369  rabid2  3381  rabid2f  3382  rabbi  3383  reubiia  3390  rmobiia  3395  reu5  3430  rmo5  3434  cbvralfw  3437  cbvrexfw  3438  cbvralf  3439  cbvrexf  3440  cbvreuw  3443  cbvrmow  3444  cbvreu  3447  cbvrmo  3448  cbvralvw  3449  cbvrexvw  3450  vjust  3495  abv  3504  ceqsex3v  3545  ceqsex4v  3546  ceqsex8v  3548  eueq  3699  reu2  3716  reu6  3717  reu3  3718  rmo4  3721  rmo3f  3725  2reu5  3749  cbvsbcw  3804  cbvsbc  3806  sbccomlem  3853  rmo3  3872  rmo3OLD  3873  rmoanim  3878  rmoanimALT  3879  cbvralcsf  3925  cbvrexcsf  3926  cbvreucsf  3927  eqss  3982  uniiunlem  4061  sspsstri  4079  compleq  4124  ssequn1  4156  unss  4160  rexun  4166  ralunb  4167  elin3  4177  incomOLD  4179  inass  4196  ssin  4207  elsymdif  4224  nssinpss  4233  dfun2  4236  difin  4238  indi  4250  indifdir  4260  ssdif0  4323  inssdif0  4329  rabeq0  4338  disj3  4403  ssundif  4433  dfif2  4469  eldifpr  4597  rexsns  4609  snprc  4653  reusn  4663  difsnpss  4740  tpss  4768  pwpr  4832  eluni2  4842  elunirab  4854  uniun  4861  unissb  4870  elintrab  4888  ssintrab  4899  intun  4908  intpr  4909  iuncom  4926  iuncom4  4927  iunab  4975  ssiinf  4978  iunn0  4989  iinab  4990  iunin2  4993  iinun2  4995  iundif2  4996  iunun  5015  iunxun  5016  iunxiun  5019  sspwuni  5022  iinpw  5028  cbvdisj  5041  disjor  5046  brun  5117  brin  5118  brdif  5119  dftr2  5174  intexrab  5243  inuni  5246  ssext  5347  pweqb  5349  otth2  5375  propeqop  5397  opelopabsbALT  5416  eqopab2bw  5435  eqopab2b  5439  pwin  5454  pwun  5458  elxp2  5579  xpiundi  5622  xpiundir  5623  poinxp  5632  soinxp  5633  frinxp  5634  seinxp  5635  weinxp  5636  inopab  5701  difopab  5702  raliunxp  5710  rexiunxp  5711  rexxpf  5718  iunxpf  5719  cnvco  5756  dmiun  5782  dmuni  5783  dm0rn0  5795  dmres  5875  restidsing  5922  cnvsym  5974  asymref  5976  codir  5980  qfto  5981  cnvopab  5997  cnvdif  6002  rniun  6006  dminss  6010  imainss  6011  difxp  6021  xpdifid  6025  dmsnn0  6064  cnvcnvsn  6076  cnvresima  6087  resco  6103  imaco  6104  rnco  6105  coiun  6109  coass  6118  ressn  6136  cnviin  6137  cnvpo  6138  cnvso  6139  xpco  6140  opreu2reurex  6145  dflim2  6247  unisuc  6267  funcnv  6423  funcnv3  6424  fncnv  6427  fun11  6428  imadif  6438  fnres  6474  dfmpt3  6482  mptfnf  6483  fnopabg  6485  fint  6558  fin  6559  fores  6600  dff1o3  6621  f1ompt  6875  fsn  6897  imaiun  7004  isocnv2  7084  isocnv3  7085  isores2  7086  isomin  7090  eqoprab2bw  7224  eqoprab2b  7225  elpwpwel  7489  sucexb  7524  sucelon  7532  dflim4  7563  fiun  7644  f1iun  7645  f11o  7648  opabex3d  7666  opabex3rd  7667  opabex3  7668  dfopab2  7750  dfoprab3s  7751  fmpox  7765  fparlem1  7807  fparlem2  7808  fsplitOLD  7813  suppvalbr  7834  tpostpos  7912  wfrlem8  7962  wfrfun  7965  dfsmo2  7984  brwitnlem  8132  oarec  8188  qsid  8363  uniinqs  8377  mapval2  8436  mapsncnv  8457  elixp2  8465  ixpin  8487  brsdom  8532  brdom2  8539  xpassen  8611  brsdom2  8641  unfilem1  8782  fiint  8795  dfsup2  8908  supmo  8916  eqinf  8948  infmo  8959  rankc1  9299  cp  9320  isinfcard  9518  aceq1  9543  aceq2  9545  dfac5lem3  9551  dfac10b  9565  dfac12a  9574  dffin7-2  9820  dfacfin7  9821  fin1a2lem6  9827  iunfo  9961  konigthlem  9990  axgroth6  10250  axgroth3  10253  sstskm  10264  ltexprlem1  10458  gt0srpr  10500  ltpsrpr  10531  map2psrpr  10532  ltresr  10562  fimaxre3  11587  sup3  11598  supaddc  11608  supmul1  11610  elnn0z  11995  elznn0nn  11996  zmin  12345  xrnemnf  12513  xrnepnf  12514  elioomnf  12833  elxrge0  12846  elfzuzb  12903  fzass4  12946  elfz2nn0  12999  elfzo2  13042  elfzo3  13055  lbfzo0  13078  fzind2  13156  nn0opthlem1  13629  hashgt23el  13786  cotr2g  14336  rexfiuz  14707  fsumcom2  15129  prodmo  15290  fprodcom2  15338  sinltx  15542  divalglem4  15747  divalglem10  15753  4sqlem12  16292  imasleval  16814  xpsfrnel  16835  xpscf  16838  isssc  17090  isffth2  17186  ispos2  17558  ismhm  17958  issubmndb  17970  nsgacs  18314  isgim  18402  oppgcntz  18492  f1omvdco3  18577  pmtrprfvalrn  18616  efgrelexlemb  18876  pgpfac1  19202  pgpfac  19206  issrg  19257  opprsubg  19386  opprunit  19411  isirred2  19451  opprirred  19452  drngprop  19513  opprdrng  19526  issdrg2  19577  islss  19706  islbs  19848  isdomn2  20072  unocv  20824  iunocv  20825  isbasis2g  21556  tgval2  21564  ntreq0  21685  isclo2  21696  cmpcov2  21998  is1stc2  22050  1stcelcls  22069  llyi  22082  unisngl  22135  txuni2  22173  xkobval  22194  hausdiag  22253  isfbas2  22443  elfg  22479  fbasrn  22492  fmfnfmlem3  22564  isfcls  22617  alexsubALTlem2  22656  istmd  22682  istgp  22685  istrg  22772  istdrg  22774  istdrg2  22786  isms2  23060  metuel2  23175  restmetu  23180  isngp  23205  isngp2  23206  isngp3  23207  elii1  23539  isncvsngp  23753  iscph  23774  isbn  23941  pmltpc  24051  ovolfcl  24067  finiunmbl  24145  iundisj  24149  dyaddisj  24197  vitalilem1  24209  ellimc3  24477  ig1pval3  24768  plyun0  24787  plydivex  24886  aannenlem2  24918  ellogrn  25143  atandm  25454  atandm3  25456  atans2  25509  tgjustf  26259  colinearalg  26696  axeuclid  26749  nbgrsym  27145  upgrtrls  27483  upgristrl  27484  usgr2pth0  27546  iswwlks  27614  isclwwlk  27762  clwwlkneq0  27807  h2hlm  28757  issh  28985  chcon2i  29241  chcon1i  29242  chcon3i  29243  chnlei  29262  cmcm2i  29370  cmcm3i  29371  3oalem3  29441  pjdifnormii  29460  pjneli  29500  dfadj2  29662  cnvadj  29669  hhcno  29681  hhcnf  29682  eleigvec  29734  eleigvec2  29735  pjimai  29953  isst  29990  ishst  29991  cvnbtwn4  30066  chrelat4i  30150  2reucom  30243  moel  30252  reuxfrdf  30255  difrab2  30261  inpr0  30292  iunin1f  30309  disjnf  30320  cbvdisjf  30321  disjorf  30329  iundisjf  30339  disjexc  30343  dfrp2  30491  xrdifh  30503  iundisjfi  30519  hashxpe  30529  pmtrprfv2  30732  xrnarchi  30813  isorng  30872  ccfldextdgrr  31057  cmpcref  31114  ordtconnlem1  31167  isrrext  31241  cntnevol  31487  ddemeas  31495  omssubaddlem  31557  omssubadd  31558  eulerpartleme  31621  eulerpartlemv  31622  eulerpartlemt0  31627  eulerpartlemgvv  31634  eulerpartlemn  31639  ballotlem2  31746  ballotlemodife  31755  oddprm2  31926  bnj257  31977  bnj268  31979  bnj290  31980  bnj312  31982  bnj89  31991  bnj887  32036  bnj976  32049  bnj1019  32051  bnj1146  32063  bnj1385  32104  bnj110  32130  bnj121  32142  bnj130  32146  bnj153  32152  bnj543  32165  bnj580  32185  bnj607  32188  bnj849  32197  bnj882  32198  bnj916  32205  bnj985v  32225  bnj985  32226  bnj1033  32241  bnj1083  32250  bnj1090  32251  bnj1128  32262  bnj1174  32275  bnj1228  32283  erdszelem1  32438  cvmliftlem15  32545  snmlval  32578  satfvsuclem2  32607  satfdm  32616  elmpst  32783  mpstrcl  32788  untuni  32935  dfso3  32950  dftr6  32986  coep  32987  coepr  32988  dffr5  32989  dfso2  32990  dfpo2  32991  cnvco1  32995  cnvco2  32996  eldm3  32997  dfdm5  33016  dfrn5  33017  imaindm  33022  frrlem9  33131  elno3  33162  conway  33264  madeval2  33290  brsset  33350  idsset  33351  dfon3  33353  dfbigcup2  33360  dfom5b  33373  dffun10  33375  dfiota3  33384  fnimage  33390  brdomain  33394  brrange  33395  brimg  33398  brapply  33399  brcup  33400  brcap  33401  brsuccf  33402  funpartlem  33403  brrestrict  33410  dfrecs2  33411  brub  33415  altopelaltxp  33437  trer  33664  filnetlem4  33729  df3nandALT1  33747  imnand2  33750  bj-dfbi5  33907  bj-bixor  33925  bj-nnfnt  34069  bj-sbnf  34164  bj-csbsnlem  34223  bj-rcleqf  34340  bj-sscon  34344  bj-pw0ALT  34345  bj-restpw  34386  bj-opelidb1  34448  wl-hadrot  34754  wl-hadcoma  34755  wl-hadnot  34757  wl-equsalvw  34793  wl-dfrexv  34864  wl-dfrexex  34865  wl-dfrmosb  34868  wl-dfrmov  34869  wl-dfreusb  34872  wl-dfreuv  34873  wl-dfrabv  34877  iundif1  34881  poimirlem25  34932  poimirlem26  34933  poimirlem30  34937  ismblfin  34948  mbfposadd  34954  itg2addnclem2  34959  ftc1anc  34990  inixp  35018  prdstotbnd  35087  heibor1lem  35102  isrngohom  35258  isidl  35307  isfldidl2  35362  isdmn3  35367  sbccom2lem  35417  triantru3  35515  vvdifopab  35536  brres2  35544  eldmqsres  35558  inxpss  35584  n0el2  35605  trcoss2  35739  dfeqvrel2  35840  dfeqvrel3  35841  redundeq1  35879  redundpbi1  35881  refrelredund4  35885  funALTVfun  35946  dfeldisj3  35967  dfeldisj5  35969  pmapglbx  36920  lhpexle3  37163  cdleme25cv  37509  dicelval3  38331  diclspsn  38345  lcfls1c  38687  sn-axrep5v  39157  psspwb  39163  moxfr  39338  fphpd  39462  ifpim1  39883  ifpnot  39884  ifpid2  39885  ifpim2  39886  ifpxorcor  39891  ifpnot23  39893  ifpananb  39921  ifpnannanb  39922  ifpxorxorb  39926  rp-fakeinunass  39930  snen1g  39939  pren2  39961  alephiso2  39966  undmrnresiss  40013  cnvssco  40015  cotrintab  40023  cnviun  40044  imaiun1  40045  coiun1  40046  elintima  40047  frege133d  40159  frege54cor0a  40258  or3or  40420  andi3or  40421  ntrneik4w  40499  k0004lem1  40546  ismnuprim  40679  undisjrab  40687  nzss  40698  pm10.541  40748  compab  40823  onfrALTlem5  40925  onfrALTlem5VD  41268  inn0f  41384  eluni2f  41418  euabsneu  43312  aiotaexb  43338  aiotavb  43339  r19.32  43345  3an4ancom24  43517  ichcom  43666  ichbi12i  43667  ichn  43675  prproropf1olem0  43713  pairreueq  43721  issubmgm  44105  sgrp2sgrp  44184  islindeps  44557  elbigo  44660  setrec1lem3  44841  elpg  44865