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  916  orbi1d  917  ifpbi123d  1079  3orbi123d  1438  3anbi123d  1439  nanbi1  1503  nanbi2  1504  xorbi12d  1527  hadbi123d  1597  had0  1606  cadbi123d  1612  nfbiit  1853  nfbidv  1924  sbequ  2089  nfbidf  2232  drex1v  2375  drnf1v  2376  drex1  2446  drnf1  2448  sb4b  2480  drsb1  2500  eujustALT  2573  eubi  2585  eleq1ab  2717  eqeq1d  2739  eqeq1dALT  2740  eqeq2d  2748  abbi  2802  eleq1w  2820  eleq2w  2821  eleq1d  2822  eleq2d  2823  eleq2dALT  2824  eqabdv  2870  nfceqdf  2895  drnfc1  2919  drnfc2  2920  neleq12d  3042  ralbidv2  3157  rexbidv2  3158  r19.21t  3232  r19.23t  3234  rexbida  3250  rexeq  3294  raleqbidvvOLD  3307  cbvraldva2  3320  raleqf  3327  rexeqfOLD  3329  ralcom2  3349  rmobidva  3365  reubidva  3366  rmobida  3375  reubida  3376  rmoeq1  3383  reueq1  3384  rmoeq1OLD  3385  reueq1OLD  3386  reueqbidv  3390  rmoeq1f  3391  reueq1f  3392  dfsbcq  3744  sbceqbid  3749  sbcbid  3797  sbcbi2  3801  eqsbc2  3806  sbcrext  3825  sbcabel  3830  ralss  4010  rexss  4011  psseq1  4044  psseq2  4045  ssconb  4096  uneq1  4115  difin2  4255  rcompleq  4259  reuun2  4279  sbcnel12g  4368  sbnfc2  4393  reldisj  4407  undif4  4421  disjssun  4422  pssdifcom1  4444  pssdifcom2  4445  sbcssg  4476  eltpg  4645  raltpg  4657  rextpg  4658  r19.12sn  4679  intmin4  4934  dfiun2g  4987  iindif1  5032  iindif2  5034  iinin2  5035  disjprg  5096  disjxun  5098  breq  5102  breq1  5103  breq2  5104  treq  5214  reusv2lem5  5351  rexxfrd  5358  rexxfr2d  5360  rexxfrd2  5362  rabxfrd  5366  opthg2  5437  oteqex2  5457  oteqex  5458  poeq1  5545  soeq1  5563  freq1  5601  weeq1  5621  weeq2  5622  opthprc  5698  wesn  5723  releq  5736  sbcrel  5740  eqrel  5743  eqrelrel  5756  xpiindi  5794  dmopab2rex  5876  dfres3  5953  brres  5955  resieq  5959  dmsnopg  6181  dfco2a  6214  dfpo2  6264  ordeq  6334  limeq  6339  ordunisssuc  6435  iotaeq  6470  sniota  6493  sbcfung  6526  imadif  6586  fneq1  6593  fneq2  6594  feq1  6650  feq2  6651  feq3  6652  sbcfng  6669  sbcfg  6670  f1eq1  6735  f1eq2  6736  f1eq3  6737  foeq1  6752  foeq2  6753  foeq3  6754  f1oeq1  6772  f1oeq2  6773  f1oeq3  6774  mpteqb  6971  rexrnmptw  7051  rexrnmpt  7053  dffo3  7058  dffo3f  7062  fmptco  7086  rexima  7196  dff13  7212  f1imaeq  7223  f1imapss  7224  cbvexfo  7248  f1eqcocnv  7259  fliftcnv  7269  isoeq1  7275  isoeq2  7276  isoeq3  7277  isoeq4  7278  isoeq5  7279  isomin  7295  isowe  7307  eqfunresadj  7318  imaeqsalvOLD  7322  nfriotadw  7335  mpoeq123  7442  rexrnmpo  7510  iunpw  7728  tfinds  7814  resf1extb  7888  fiun  7899  f1iun  7900  opiota  8015  xpord3pred  8106  ottpos  8190  dmtpos  8192  onoviun  8287  smoeq  8294  smoiso2  8313  tfr2b  8339  oarec  8501  oeeui  8542  nnacan  8568  nnmcan  8574  ereq1  8655  ereq2  8656  elecg  8692  ereldm  8701  ixpiin  8876  boxriin  8892  boxcutc  8893  omxpenlem  9020  enfiALT  9126  nnsdomo  9157  isfinite2  9212  ixpfi2  9264  elfi2  9331  fipwss  9346  ttrclse  9650  ennum  9873  cardsdom2  9914  aleph11  10008  alephiso  10022  fin23lem26  10249  compssiso  10298  isf34lem4  10301  isfin5-2  10315  fin1a2lem5  10328  brdom7disj  10455  brdom6disj  10456  fpwwe2lem7  10562  fpwwe2lem11  10566  fpwwe2lem12  10567  genpass  10934  ltasr  11025  axpre-lttri  11090  infm3  12115  creur  12153  eqreznegel  12861  rpneg  12953  ltxr  13043  icoshftf1o  13404  elfzm11  13525  elfzomelpfzo  13702  nn0ennn  13916  nnesq  14164  hashbclem  14389  hashf1lem1  14392  leiso  14396  fz1isolem  14398  pr2pwpr  14416  repsdf2  14715  dfrtrclrec2  14995  rexfiuz  15285  cau4  15294  ello1mpt2  15459  o1lo1  15474  fsumcom2  15711  incexc2  15775  fprodcom2  15921  dvdsflip  16258  bitsmod  16377  bitscmp  16379  smueqlem  16431  divgcdcoprm0  16606  hashdvds  16716  prmreclem2  16859  vdwapun  16916  vdwmc2  16921  imasaddfnlem  17463  comfeq  17643  oppcsect  17716  funcres2b  17835  funcpropd  17840  fullpropd  17860  fthpropd  17861  fthres2b  17870  fthres2c  17871  fullres2c  17879  ffthres2c  17880  fucsect  17913  fucinv  17914  setcsect  18027  pospropd  18262  tosso  18354  odulatb  18371  oduclatb  18444  odudlatb  18462  isipodrs  18474  mgmhmpropd  18637  issgrpv  18660  issgrpn0  18661  mndpropd  18698  mhmpropd  18731  issubm2  18743  efmnd1bas  18832  grppropd  18898  grpinvcnv  18953  conjghm  19195  conjnmzb  19199  ghmpropd  19202  gapm  19252  symg1bas  19337  pmtrfrn  19404  cmnpropd  19737  ablpropd  19738  eqgabl  19780  gsumcom2  19921  dmdprd  19946  dprdw  19958  subgdmdprd  19982  pgpfac1lem2  20023  pgpfac1lem4  20026  rngpropd  20126  ringpropd  20240  crngpropd  20241  crngunit  20331  unitpropd  20370  isnirred  20373  nzrpropd  20470  issubrng  20497  subrngpropd  20518  resrhm2b  20552  subrgpropd  20558  rhmpropd  20559  rngcsect  20586  ringcsect  20620  isdomn3  20665  drngpropd  20719  fldpropd  20720  fiidomfld  20724  acsfn1p  20749  abvpropd  20785  lmodprop2d  20892  lsspropd  20986  lmhmpropd  21042  lbspropd  21068  lmhmlvec  21079  lvecprop2d  21138  lvecpropd  21139  df2idl2rng  21228  pzriprnglem10  21462  phlpropd  21627  assapropd  21844  psrbagconf1o  21902  mplmonmul  22008  ismhp3  22102  mat1dimbas  22433  tpspropd  22899  tgss2  22948  lmbr2  23220  ist1-2  23308  ist1-3  23310  subislly  23442  dissnlocfin  23490  iskgen3  23510  txcnmpt  23585  hausdiag  23606  hauseqlcld  23607  xkococnlem  23620  tgqtop  23673  txhmeo  23764  uffix2  23885  ufildr  23892  txflf  23967  tgphaus  24078  qustgplem  24082  qustgphaus  24084  xpsdsval  24342  blin  24382  blres  24392  xmeterval  24393  xmspropd  24434  mspropd  24435  setsms  24441  metequiv  24470  metustsym  24516  restmetu  24531  ngppropd  24598  xrtgioo  24768  metdsge  24811  icopnfcnv  24913  iccpnfcnv  24915  lmhmclm  25060  lmmbr  25231  equivcmet  25290  cmspropd  25322  iunmbl2  25531  ioombl1lem4  25535  mbfaddlem  25634  i1fmullem  25668  itg1mulc  25678  iblcnlem1  25762  iblrelem  25765  iblre  25768  iblcn  25773  limcun  25869  mvth  25970  ofmulrt  26262  resinf1o  26518  quad2  26822  1cubr  26825  dcubic  26829  wilthlem2  27052  dvdsflf1o  27170  dvdsflsumcom  27171  fsumvma  27197  vmasum  27200  logfac2  27201  logfaclbnd  27206  dchrelbas3  27222  lgsquadlem1  27364  lgsquadlem2  27365  eqcuts2  27799  mulsrid  28126  z12sge0  28496  readdscl  28512  ax5seg  29029  ushgredgedg  29320  ushgredgedgloop  29322  nbumgrvtx  29437  upgriswlk  29732  wspniunwspnon  30014  rusgrnumwwlkb0  30065  isclwwlknx  30129  clwwlknscsh  30155  clwwlknonel  30188  0trl  30215  0spth  30219  0clwlk  30223  0crct  30226  0cycl  30227  eupth2lem2  30312  eucrct2eupth  30338  fusgr2wsp2nb  30427  ocin  31390  chpsscon3  31597  chscllem2  31732  adjval  31984  pjimai  32270  mdsldmd1i  32425  elat2  32434  mdsymi  32505  sbceqbidf  32579  rmoxfrd  32585  rmounid  32587  disjxun0  32667  disjrdx  32684  eqrelrd2  32712  fmptcof2  32753  ofpreima  32761  funcnv5mpt  32763  ressupprn  32786  1stpreima  32803  2ndpreima  32804  fpwrelmapffslem  32828  cntrval2  33271  domnpropd  33377  idompropd  33378  subsdrg  33398  qsxpid  33461  grplsm0l  33502  opprlidlabs  33584  ressply1mon1p  33667  psrmonmul  33733  algextdeglem6  33906  smatrcl  33980  locfinreflem  34024  zarcls  34058  zhmnrg  34149  qqhval2  34166  ismntop  34210  reprsuc  34799  reprdifc  34811  bnj919  34950  bnj956  34959  bnj976  34960  bnj1366  35011  bnj916  35115  satfvsucsuc  35587  satfdm  35591  dmopab3rexdif  35627  rexxfr3dALT  35861  sscoid  36133  dfrdg4  36173  altopthbg  36190  broutsideof3  36348  rmoeqbidv  36435  sbequbidv  36436  disjeq12dv  36437  ixpeq12dv  36438  cbvmodavw  36472  cbveudavw  36473  cbvrmodavw  36474  cbvreudavw  36475  cbvsbdavw  36476  cbvsbdavw2  36477  cbvabdavw  36478  cbvsbcdavw  36479  cbvsbcdavw2  36480  cbvdisjdavw  36490  cbvrmodavw2  36505  cbvreudavw2  36506  cbvdisjdavw2  36511  bj-nnfbi  37012  bj-cbvexdv  37075  bj-sbievw  37122  mobidvALT  37132  bj-axreprepsep  37350  bj-restuni  37377  bj-elid6  37452  cbveud  37654  cbvreud  37655  exrecfnlem  37661  wl-ifp-ncond2  37747  wl-ifpimpr  37748  wl-3xorbi123d  37757  wl-sb8eut  37862  wl-sb8eutv  37863  wl-sb8mot  37864  wl-sb8motv  37865  wl-clabtv  37870  wl-clabt  37871  wl-eujustlem1  37872  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem25  37925  ftc1anclem5  37977  istotbnd3  38051  sstotbnd  38055  heibor  38101  isass  38126  isidlc  38295  smprngopr  38332  brvvdif  38548  elecALTV  38551  eqrel2  38585  dmecd  38590  relcnveq2  38609  eldmxrncnvepres  38714  eldmxrncnvepres2  38715  extssr  38869  elrefrelsrel  38880  refreleq  38881  elcnvrefrelsrel  38896  elrelscnveq2  38909  elsymrelsrel  38921  symreleq  38922  eltrrelsrel  38945  trreleq  38946  eleqvrelsrel  38958  eqvreleq  38966  redundpim3  38994  erALTVeq1  39034  elfunsALTVfunALTV  39062  eldisjsdisj  39104  eldisjeq  39121  disjsuc  39139  parteq1  39157  parteq2  39158  islshpsm  39385  lcvexchlem1  39439  opcon1b  39603  isat3  39712  glbconN  39782  cdleme32fva  40842  cdlemg2cex  40996  dibelval3  41552  dib1dim  41570  doch11  41778  dochsordN  41779  mapdordlem1a  42039  mapd11  42044  mapdsord  42060  mapdcnv11N  42064  mapd0  42070  sn-iotalem  42622  ricfld  42929  fimgmcyc  42933  fsuppind  42977  mrefg2  43093  jm2.23  43382  wepwsolem  43428  dnwech  43434  islssfg2  43457  gicabl  43485  onsupmaxb  43625  onsupeqnmax  43633  orddif0suc  43654  oadif1lem  43765  oadif1  43766  fzunt  43840  fzuntd  43841  fzunt1d  43842  fzuntgd  43843  ifpbi2  43852  ifpbi3  43853  ifpbi1  43862  ifpbi12  43873  ifpbi13  43874  ontric3g  43907  pwinfig  43946  inintabd  43964  cnvcnvintabd  43985  cnvintabd  43988  intimag  44041  briunov2  44067  heeq12  44161  sbcheg  44164  uneqsn  44410  ntrneineine0lem  44468  ntrneineine1lem  44469  ntrneik2  44477  ntrneix2  44478  ntrneik13  44483  ntrneix13  44484  ralbidar  44829  rexbidar  44830  trsbc  44925  relpeq1  45329  relpeq2  45330  relpeq3  45331  relpeq4  45332  relpeq5  45333  n0abso  45361  modelaxreplem3  45365  iindif2f  45548  rnmptpr  45565  iccintsng  45912  xlimres  46208  fsetsniunop  47438  fsetsnprcnex  47444  fcoresf1ob  47462  f1cof1b  47466  f1ocof1ob  47470  dfateq12d  47515  aov0nbovbi  47584  fnotaovb  47587  ichbidv  47842  sprsymrelf  47884  prprsprreu  47908  prprreueq  47909  edgusgrclnbfin  48231  dfclnbgr6  48245  dfnbgr6  48246  isubgredg  48255  gpgnbgrvtx0  48463  gpgnbgrvtx1  48464  rngcsectALTV  48664  ringcsectALTV  48698  lindslinindsimp2lem5  48851  xpco2  49245  opndisj  49291  i0oii  49308  io1ii  49309  iscnrm3lem2  49323  uobffth  49606  uobeqw  49607  thincpropd  49830  termcpropd  49891