Theorem 3bitr4g 314

Description: More general version of 3bitr4i 303. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)

Hypotheses

Ref	Expression
3bitr4g.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4g.2	⊢ (𝜃 ↔ 𝜓)
3bitr4g.3	⊢ (𝜏 ↔ 𝜒)

Assertion

Ref	Expression
3bitr4g	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 ⊢ (𝜃 ↔ 𝜓)
2		3bitr4g.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitrid 283	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 289	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bibi1d  343  pm5.32rd  578  orbi2d  915  orbi1d  916  ifpbi123d  1078  3orbi123d  1437  3anbi123d  1438  nanbi1  1501  nanbi2  1502  xorbi12d  1525  hadbi123d  1595  had0  1604  cadbi123d  1610  nfbiit  1851  nfbidv  1922  sbequ  2084  nfbidf  2225  drex1v  2369  drnf1v  2370  drex1  2440  drnf1  2442  sb4b  2474  drsb1  2494  eujustALT  2566  eubi  2578  eleq1ab  2710  eqeq1d  2732  eqeq1dALT  2733  eqeq2d  2741  abbi  2795  eleq1w  2812  eleq2w  2813  eleq1d  2814  eleq2d  2815  eleq2dALT  2816  eqabdv  2862  nfceqdf  2888  drnfc1  2912  drnfc2  2913  neleq12d  3035  ralbidv2  3153  rexbidv2  3154  r19.21t  3232  r19.23t  3234  rexbida  3250  rexeq  3297  raleqbidvvOLD  3310  cbvraldva2  3323  cbvrexdva2OLD  3325  raleqf  3331  rexeqfOLD  3333  ralcom2  3353  rmobidva  3371  reubidva  3372  rmobida  3381  reubida  3382  rmoeq1  3390  reueq1  3391  rmoeq1OLD  3392  reueq1OLD  3393  reueqbidv  3397  rmoeq1f  3398  reueq1f  3399  dfsbcq  3758  sbceqbid  3763  sbcbid  3811  sbcbi2  3815  eqsbc2  3820  sbcrext  3839  sbcabel  3844  ralss  4024  rexss  4025  psseq1  4056  psseq2  4057  ssconb  4108  uneq1  4127  difin2  4267  rcompleq  4271  reuun2  4291  sbcnel12g  4380  sbnfc2  4405  reldisj  4419  undif4  4433  disjssun  4434  pssdifcom1  4456  pssdifcom2  4457  sbcssg  4486  eltpg  4653  raltpg  4665  rextpg  4666  r19.12sn  4687  intmin4  4944  dfiun2g  4997  dfiun2gOLD  4998  iindif1  5042  iindif2  5044  iinin2  5045  disjprg  5106  disjxun  5108  breq  5112  breq1  5113  breq2  5114  treq  5225  reusv2lem5  5360  rexxfrd  5367  rexxfr2d  5369  rexxfrd2  5371  rabxfrd  5375  opthg2  5442  oteqex2  5462  oteqex  5463  poeq1  5552  soeq1  5570  freq1  5608  weeq1  5628  weeq2  5629  opthprc  5705  wesn  5730  releq  5742  sbcrel  5746  eqrel  5750  eqrelrel  5763  xpiindi  5802  dmopab2rex  5884  dfres3  5958  brres  5960  resieq  5964  dmsnopg  6189  dfco2a  6222  dfpo2  6272  ordeq  6342  limeq  6347  ordunisssuc  6443  iotaeq  6479  sniota  6505  sbcfung  6543  imadif  6603  fneq1  6612  fneq2  6613  feq1  6669  feq2  6670  feq3  6671  sbcfng  6688  sbcfg  6689  f1eq1  6754  f1eq2  6755  f1eq3  6756  foeq1  6771  foeq2  6772  foeq3  6773  f1oeq1  6791  f1oeq2  6792  f1oeq3  6793  mpteqb  6990  rexrnmptw  7070  rexrnmpt  7072  dffo3  7077  dffo3f  7081  fmptco  7104  rexima  7215  dff13  7232  f1imaeq  7243  f1imapss  7244  cbvexfo  7268  f1eqcocnv  7279  fliftcnv  7289  isoeq1  7295  isoeq2  7296  isoeq3  7297  isoeq4  7298  isoeq5  7299  isomin  7315  isowe  7327  eqfunresadj  7338  imaeqsalvOLD  7342  nfriotadw  7355  mpoeq123  7464  rexrnmpo  7532  iunpw  7750  tfinds  7839  resf1extb  7913  fiun  7924  f1iun  7925  opiota  8041  xpord3pred  8134  ottpos  8218  dmtpos  8220  onoviun  8315  smoeq  8322  smoiso2  8341  tfr2b  8367  oarec  8529  oeeui  8569  nnacan  8595  nnmcan  8601  ereq1  8681  ereq2  8682  elecg  8718  ereldm  8727  ixpiin  8900  boxriin  8916  boxcutc  8917  omxpenlem  9047  enfiALT  9158  nnsdomo  9188  isfinite2  9252  ixpfi2  9308  elfi2  9372  fipwss  9387  ttrclse  9687  ennum  9907  cardsdom2  9948  aleph11  10044  alephiso  10058  fin23lem26  10285  compssiso  10334  isf34lem4  10337  isfin5-2  10351  fin1a2lem5  10364  brdom7disj  10491  brdom6disj  10492  fpwwe2lem7  10597  fpwwe2lem11  10601  fpwwe2lem12  10602  genpass  10969  ltasr  11060  axpre-lttri  11125  infm3  12149  creur  12187  eqreznegel  12900  rpneg  12992  ltxr  13082  icoshftf1o  13442  elfzm11  13563  elfzomelpfzo  13739  nn0ennn  13951  nnesq  14199  hashbclem  14424  hashf1lem1  14427  leiso  14431  fz1isolem  14433  pr2pwpr  14451  repsdf2  14750  dfrtrclrec2  15031  rexfiuz  15321  cau4  15330  ello1mpt2  15495  o1lo1  15510  fsumcom2  15747  incexc2  15811  fprodcom2  15957  dvdsflip  16294  bitsmod  16413  bitscmp  16415  smueqlem  16467  divgcdcoprm0  16642  hashdvds  16752  prmreclem2  16895  vdwapun  16952  vdwmc2  16957  imasaddfnlem  17498  comfeq  17674  oppcsect  17747  funcres2b  17866  funcpropd  17871  fullpropd  17891  fthpropd  17892  fthres2b  17901  fthres2c  17902  fullres2c  17910  ffthres2c  17911  fucsect  17944  fucinv  17945  setcsect  18058  pospropd  18293  tosso  18385  odulatb  18400  oduclatb  18473  odudlatb  18491  isipodrs  18503  mgmhmpropd  18632  issgrpv  18655  issgrpn0  18656  mndpropd  18693  mhmpropd  18726  issubm2  18738  efmnd1bas  18827  grppropd  18890  grpinvcnv  18945  conjghm  19188  conjnmzb  19192  ghmpropd  19195  gapm  19245  symg1bas  19328  pmtrfrn  19395  cmnpropd  19728  ablpropd  19729  eqgabl  19771  gsumcom2  19912  dmdprd  19937  dprdw  19949  subgdmdprd  19973  pgpfac1lem2  20014  pgpfac1lem4  20017  rngpropd  20090  ringpropd  20204  crngpropd  20205  crngunit  20294  unitpropd  20333  isnirred  20336  nzrpropd  20436  issubrng  20463  subrngpropd  20484  resrhm2b  20518  subrgpropd  20524  rhmpropd  20525  rngcsect  20552  ringcsect  20586  isdomn3  20631  drngpropd  20685  fldpropd  20686  fiidomfld  20690  acsfn1p  20715  abvpropd  20751  lmodprop2d  20837  lsspropd  20931  lmhmpropd  20987  lbspropd  21013  lmhmlvec  21024  lvecprop2d  21083  lvecpropd  21084  df2idl2rng  21173  pzriprnglem10  21407  phlpropd  21571  assapropd  21788  psrbagconf1o  21845  mplmonmul  21950  ismhp3  22036  mat1dimbas  22366  tpspropd  22832  tgss2  22881  lmbr2  23153  ist1-2  23241  ist1-3  23243  subislly  23375  dissnlocfin  23423  iskgen3  23443  txcnmpt  23518  hausdiag  23539  hauseqlcld  23540  xkococnlem  23553  tgqtop  23606  txhmeo  23697  uffix2  23818  ufildr  23825  txflf  23900  tgphaus  24011  qustgplem  24015  qustgphaus  24017  xpsdsval  24276  blin  24316  blres  24326  xmeterval  24327  xmspropd  24368  mspropd  24369  setsms  24375  metequiv  24404  metustsym  24450  restmetu  24465  ngppropd  24532  xrtgioo  24702  metdsge  24745  icopnfcnv  24847  iccpnfcnv  24849  lmhmclm  24994  lmmbr  25165  equivcmet  25224  cmspropd  25256  iunmbl2  25465  ioombl1lem4  25469  mbfaddlem  25568  i1fmullem  25602  itg1mulc  25612  iblcnlem1  25696  iblrelem  25699  iblre  25702  iblcn  25707  limcun  25803  mvth  25904  ofmulrt  26196  resinf1o  26452  quad2  26756  1cubr  26759  dcubic  26763  wilthlem2  26986  dvdsflf1o  27104  dvdsflsumcom  27105  fsumvma  27131  vmasum  27134  logfac2  27135  logfaclbnd  27140  dchrelbas3  27156  lgsquadlem1  27298  lgsquadlem2  27299  eqscut2  27725  mulsrid  28023  zs12ge0  28349  readdscl  28357  ax5seg  28872  ushgredgedg  29163  ushgredgedgloop  29165  nbumgrvtx  29280  upgriswlk  29576  wspniunwspnon  29860  rusgrnumwwlkb0  29908  isclwwlknx  29972  clwwlknscsh  29998  clwwlknonel  30031  0trl  30058  0spth  30062  0clwlk  30066  0crct  30069  0cycl  30070  eupth2lem2  30155  eucrct2eupth  30181  fusgr2wsp2nb  30270  ocin  31232  chpsscon3  31439  chscllem2  31574  adjval  31826  pjimai  32112  mdsldmd1i  32267  elat2  32276  mdsymi  32347  sbceqbidf  32423  rmoxfrd  32429  rmounid  32431  disjxun0  32510  disjrdx  32527  eqrelrd2  32551  fmptcof2  32588  ofpreima  32596  funcnv5mpt  32599  ressupprn  32620  1stpreima  32637  2ndpreima  32638  fpwrelmapffslem  32662  cntrval2  33135  domnpropd  33234  idompropd  33235  subsdrg  33255  qsxpid  33340  grplsm0l  33381  opprlidlabs  33463  ressply1mon1p  33544  algextdeglem6  33719  smatrcl  33793  locfinreflem  33837  zarcls  33871  zhmnrg  33962  qqhval2  33979  ismntop  34023  reprsuc  34613  reprdifc  34625  bnj919  34764  bnj956  34773  bnj976  34774  bnj1366  34826  bnj916  34930  satfvsucsuc  35359  satfdm  35363  dmopab3rexdif  35399  rexxfr3dALT  35633  sscoid  35908  dfrdg4  35946  altopthbg  35963  broutsideof3  36121  rmoeqbidv  36208  sbequbidv  36209  disjeq12dv  36210  ixpeq12dv  36211  cbvmodavw  36245  cbveudavw  36246  cbvrmodavw  36247  cbvreudavw  36248  cbvsbdavw  36249  cbvsbdavw2  36250  cbvabdavw  36251  cbvsbcdavw  36252  cbvsbcdavw2  36253  cbvdisjdavw  36263  cbvrmodavw2  36278  cbvreudavw2  36279  cbvdisjdavw2  36284  bj-nnfbi  36720  bj-cbvexdv  36795  bj-sbievw  36842  mobidvALT  36852  bj-restuni  37092  bj-elid6  37165  cbveud  37367  cbvreud  37368  exrecfnlem  37374  wl-ifp-ncond2  37460  wl-ifpimpr  37461  wl-3xorbi123d  37470  wl-sb8eut  37573  wl-sb8eutv  37574  wl-sb8mot  37575  wl-sb8motv  37576  wl-clabtv  37592  wl-clabt  37593  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem25  37646  ftc1anclem5  37698  istotbnd3  37772  sstotbnd  37776  heibor  37822  isass  37847  isidlc  38016  smprngopr  38053  brvvdif  38259  elecALTV  38262  eqrel2  38294  dmecd  38299  relcnveq2  38318  eldmxrncnvepres  38403  eldmxrncnvepres2  38404  elrelscnveq2  38491  extssr  38507  elrefrelsrel  38518  refreleq  38519  elcnvrefrelsrel  38534  elsymrelsrel  38555  symreleq  38556  eltrrelsrel  38579  trreleq  38580  eleqvrelsrel  38592  eqvreleq  38600  redundpim3  38628  erALTVeq1  38668  elfunsALTVfunALTV  38696  eldisjsdisj  38726  eldisjeq  38740  disjsuc  38758  parteq1  38773  parteq2  38774  islshpsm  38980  lcvexchlem1  39034  opcon1b  39198  isat3  39307  glbconN  39377  glbconNOLD  39378  cdleme32fva  40438  cdlemg2cex  40592  dibelval3  41148  dib1dim  41166  doch11  41374  dochsordN  41375  mapdordlem1a  41635  mapd11  41640  mapdsord  41656  mapdcnv11N  41660  mapd0  41666  sn-iotalem  42216  ricfld  42525  fimgmcyc  42529  fsuppind  42585  mrefg2  42702  jm2.23  42992  wepwsolem  43038  dnwech  43044  islssfg2  43067  gicabl  43095  onsupmaxb  43235  onsupeqnmax  43243  orddif0suc  43264  oadif1lem  43375  oadif1  43376  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  ifpbi2  43463  ifpbi3  43464  ifpbi1  43473  ifpbi12  43484  ifpbi13  43485  ontric3g  43518  pwinfig  43557  inintabd  43575  cnvcnvintabd  43596  cnvintabd  43599  intimag  43652  briunov2  43678  heeq12  43772  sbcheg  43775  uneqsn  44021  ntrneineine0lem  44079  ntrneineine1lem  44080  ntrneik2  44088  ntrneix2  44089  ntrneik13  44094  ntrneix13  44095  ralbidar  44441  rexbidar  44442  trsbc  44537  relpeq1  44941  relpeq2  44942  relpeq3  44943  relpeq4  44944  relpeq5  44945  n0abso  44973  modelaxreplem3  44977  iindif2f  45161  rnmptpr  45178  iccintsng  45528  xlimres  45826  fsetsniunop  47054  fsetsnprcnex  47060  fcoresf1ob  47078  f1cof1b  47082  f1ocof1ob  47086  dfateq12d  47131  aov0nbovbi  47200  fnotaovb  47203  ichbidv  47458  sprsymrelf  47500  prprsprreu  47524  prprreueq  47525  edgusgrclnbfin  47846  dfclnbgr6  47860  dfnbgr6  47861  isubgredg  47870  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  rngcsectALTV  48267  ringcsectALTV  48301  lindslinindsimp2lem5  48455  xpco2  48849  opndisj  48895  i0oii  48912  io1ii  48913  iscnrm3lem2  48927  uobffth  49211  uobeqw  49212  thincpropd  49435  termcpropd  49496