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  2368  drnf1v  2369  drex1  2439  drnf1  2441  sb4b  2473  drsb1  2493  eujustALT  2565  eubi  2577  eleq1ab  2709  eqeq1d  2731  eqeq1dALT  2732  eqeq2d  2740  abbi  2794  eleq1w  2811  eleq2w  2812  eleq1d  2813  eleq2d  2814  eleq2dALT  2815  eqabdv  2861  nfceqdf  2887  drnfc1  2911  drnfc2  2912  neleq12d  3034  ralbidv2  3148  rexbidv2  3149  r19.21t  3223  r19.23t  3225  rexbida  3241  rexeq  3285  raleqbidvvOLD  3298  cbvraldva2  3311  raleqf  3318  rexeqfOLD  3320  ralcom2  3340  rmobidva  3358  reubidva  3359  rmobida  3368  reubida  3369  rmoeq1  3376  reueq1  3377  rmoeq1OLD  3378  reueq1OLD  3379  reueqbidv  3383  rmoeq1f  3384  reueq1f  3385  dfsbcq  3744  sbceqbid  3749  sbcbid  3797  sbcbi2  3801  eqsbc2  3806  sbcrext  3825  sbcabel  3830  ralss  4010  rexss  4011  psseq1  4041  psseq2  4042  ssconb  4093  uneq1  4112  difin2  4252  rcompleq  4256  reuun2  4276  sbcnel12g  4365  sbnfc2  4390  reldisj  4404  undif4  4418  disjssun  4419  pssdifcom1  4441  pssdifcom2  4442  sbcssg  4471  eltpg  4638  raltpg  4650  rextpg  4651  r19.12sn  4672  intmin4  4927  dfiun2g  4980  iindif1  5024  iindif2  5026  iinin2  5027  disjprg  5088  disjxun  5090  breq  5094  breq1  5095  breq2  5096  treq  5206  reusv2lem5  5341  rexxfrd  5348  rexxfr2d  5350  rexxfrd2  5352  rabxfrd  5356  opthg2  5422  oteqex2  5442  oteqex  5443  poeq1  5530  soeq1  5548  freq1  5586  weeq1  5606  weeq2  5607  opthprc  5683  wesn  5708  releq  5720  sbcrel  5724  eqrel  5727  eqrelrel  5740  xpiindi  5778  dmopab2rex  5860  dfres3  5935  brres  5937  resieq  5941  dmsnopg  6162  dfco2a  6195  dfpo2  6244  ordeq  6314  limeq  6319  ordunisssuc  6415  iotaeq  6450  sniota  6473  sbcfung  6506  imadif  6566  fneq1  6573  fneq2  6574  feq1  6630  feq2  6631  feq3  6632  sbcfng  6649  sbcfg  6650  f1eq1  6715  f1eq2  6716  f1eq3  6717  foeq1  6732  foeq2  6733  foeq3  6734  f1oeq1  6752  f1oeq2  6753  f1oeq3  6754  mpteqb  6949  rexrnmptw  7029  rexrnmpt  7031  dffo3  7036  dffo3f  7040  fmptco  7063  rexima  7174  dff13  7191  f1imaeq  7202  f1imapss  7203  cbvexfo  7227  f1eqcocnv  7238  fliftcnv  7248  isoeq1  7254  isoeq2  7255  isoeq3  7256  isoeq4  7257  isoeq5  7258  isomin  7274  isowe  7286  eqfunresadj  7297  imaeqsalvOLD  7301  nfriotadw  7314  mpoeq123  7421  rexrnmpo  7489  iunpw  7707  tfinds  7793  resf1extb  7867  fiun  7878  f1iun  7879  opiota  7994  xpord3pred  8085  ottpos  8169  dmtpos  8171  onoviun  8266  smoeq  8273  smoiso2  8292  tfr2b  8318  oarec  8480  oeeui  8520  nnacan  8546  nnmcan  8552  ereq1  8632  ereq2  8633  elecg  8669  ereldm  8678  ixpiin  8851  boxriin  8867  boxcutc  8868  omxpenlem  8995  enfiALT  9102  nnsdomo  9132  isfinite2  9187  ixpfi2  9240  elfi2  9304  fipwss  9319  ttrclse  9623  ennum  9843  cardsdom2  9884  aleph11  9978  alephiso  9992  fin23lem26  10219  compssiso  10268  isf34lem4  10271  isfin5-2  10285  fin1a2lem5  10298  brdom7disj  10425  brdom6disj  10426  fpwwe2lem7  10531  fpwwe2lem11  10535  fpwwe2lem12  10536  genpass  10903  ltasr  10994  axpre-lttri  11059  infm3  12084  creur  12122  eqreznegel  12835  rpneg  12927  ltxr  13017  icoshftf1o  13377  elfzm11  13498  elfzomelpfzo  13674  nn0ennn  13886  nnesq  14134  hashbclem  14359  hashf1lem1  14362  leiso  14366  fz1isolem  14368  pr2pwpr  14386  repsdf2  14684  dfrtrclrec2  14965  rexfiuz  15255  cau4  15264  ello1mpt2  15429  o1lo1  15444  fsumcom2  15681  incexc2  15745  fprodcom2  15891  dvdsflip  16228  bitsmod  16347  bitscmp  16349  smueqlem  16401  divgcdcoprm0  16576  hashdvds  16686  prmreclem2  16829  vdwapun  16886  vdwmc2  16891  imasaddfnlem  17432  comfeq  17612  oppcsect  17685  funcres2b  17804  funcpropd  17809  fullpropd  17829  fthpropd  17830  fthres2b  17839  fthres2c  17840  fullres2c  17848  ffthres2c  17849  fucsect  17882  fucinv  17883  setcsect  17996  pospropd  18231  tosso  18323  odulatb  18340  oduclatb  18413  odudlatb  18431  isipodrs  18443  mgmhmpropd  18572  issgrpv  18595  issgrpn0  18596  mndpropd  18633  mhmpropd  18666  issubm2  18678  efmnd1bas  18767  grppropd  18830  grpinvcnv  18885  conjghm  19128  conjnmzb  19132  ghmpropd  19135  gapm  19185  symg1bas  19270  pmtrfrn  19337  cmnpropd  19670  ablpropd  19671  eqgabl  19713  gsumcom2  19854  dmdprd  19879  dprdw  19891  subgdmdprd  19915  pgpfac1lem2  19956  pgpfac1lem4  19959  rngpropd  20059  ringpropd  20173  crngpropd  20174  crngunit  20263  unitpropd  20302  isnirred  20305  nzrpropd  20405  issubrng  20432  subrngpropd  20453  resrhm2b  20487  subrgpropd  20493  rhmpropd  20494  rngcsect  20521  ringcsect  20555  isdomn3  20600  drngpropd  20654  fldpropd  20655  fiidomfld  20659  acsfn1p  20684  abvpropd  20720  lmodprop2d  20827  lsspropd  20921  lmhmpropd  20977  lbspropd  21003  lmhmlvec  21014  lvecprop2d  21073  lvecpropd  21074  df2idl2rng  21163  pzriprnglem10  21397  phlpropd  21562  assapropd  21779  psrbagconf1o  21836  mplmonmul  21941  ismhp3  22027  mat1dimbas  22357  tpspropd  22823  tgss2  22872  lmbr2  23144  ist1-2  23232  ist1-3  23234  subislly  23366  dissnlocfin  23414  iskgen3  23434  txcnmpt  23509  hausdiag  23530  hauseqlcld  23531  xkococnlem  23544  tgqtop  23597  txhmeo  23688  uffix2  23809  ufildr  23816  txflf  23891  tgphaus  24002  qustgplem  24006  qustgphaus  24008  xpsdsval  24267  blin  24307  blres  24317  xmeterval  24318  xmspropd  24359  mspropd  24360  setsms  24366  metequiv  24395  metustsym  24441  restmetu  24456  ngppropd  24523  xrtgioo  24693  metdsge  24736  icopnfcnv  24838  iccpnfcnv  24840  lmhmclm  24985  lmmbr  25156  equivcmet  25215  cmspropd  25247  iunmbl2  25456  ioombl1lem4  25460  mbfaddlem  25559  i1fmullem  25593  itg1mulc  25603  iblcnlem1  25687  iblrelem  25690  iblre  25693  iblcn  25698  limcun  25794  mvth  25895  ofmulrt  26187  resinf1o  26443  quad2  26747  1cubr  26750  dcubic  26754  wilthlem2  26977  dvdsflf1o  27095  dvdsflsumcom  27096  fsumvma  27122  vmasum  27125  logfac2  27126  logfaclbnd  27131  dchrelbas3  27147  lgsquadlem1  27289  lgsquadlem2  27290  eqscut2  27717  mulsrid  28021  zs12ge0  28360  readdscl  28368  ax5seg  28883  ushgredgedg  29174  ushgredgedgloop  29176  nbumgrvtx  29291  upgriswlk  29586  wspniunwspnon  29868  rusgrnumwwlkb0  29916  isclwwlknx  29980  clwwlknscsh  30006  clwwlknonel  30039  0trl  30066  0spth  30070  0clwlk  30074  0crct  30077  0cycl  30078  eupth2lem2  30163  eucrct2eupth  30189  fusgr2wsp2nb  30278  ocin  31240  chpsscon3  31447  chscllem2  31582  adjval  31834  pjimai  32120  mdsldmd1i  32275  elat2  32284  mdsymi  32355  sbceqbidf  32431  rmoxfrd  32437  rmounid  32439  disjxun0  32518  disjrdx  32535  eqrelrd2  32561  fmptcof2  32600  ofpreima  32608  funcnv5mpt  32611  ressupprn  32632  1stpreima  32649  2ndpreima  32650  fpwrelmapffslem  32675  cntrval2  33113  domnpropd  33216  idompropd  33217  subsdrg  33237  qsxpid  33299  grplsm0l  33340  opprlidlabs  33422  ressply1mon1p  33503  algextdeglem6  33689  smatrcl  33763  locfinreflem  33807  zarcls  33841  zhmnrg  33932  qqhval2  33949  ismntop  33993  reprsuc  34583  reprdifc  34595  bnj919  34734  bnj956  34743  bnj976  34744  bnj1366  34796  bnj916  34900  satfvsucsuc  35342  satfdm  35346  dmopab3rexdif  35382  rexxfr3dALT  35616  sscoid  35891  dfrdg4  35929  altopthbg  35946  broutsideof3  36104  rmoeqbidv  36191  sbequbidv  36192  disjeq12dv  36193  ixpeq12dv  36194  cbvmodavw  36228  cbveudavw  36229  cbvrmodavw  36230  cbvreudavw  36231  cbvsbdavw  36232  cbvsbdavw2  36233  cbvabdavw  36234  cbvsbcdavw  36235  cbvsbcdavw2  36236  cbvdisjdavw  36246  cbvrmodavw2  36261  cbvreudavw2  36262  cbvdisjdavw2  36267  bj-nnfbi  36703  bj-cbvexdv  36778  bj-sbievw  36825  mobidvALT  36835  bj-restuni  37075  bj-elid6  37148  cbveud  37350  cbvreud  37351  exrecfnlem  37357  wl-ifp-ncond2  37443  wl-ifpimpr  37444  wl-3xorbi123d  37453  wl-sb8eut  37556  wl-sb8eutv  37557  wl-sb8mot  37558  wl-sb8motv  37559  wl-clabtv  37575  wl-clabt  37576  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem25  37629  ftc1anclem5  37681  istotbnd3  37755  sstotbnd  37759  heibor  37805  isass  37830  isidlc  37999  smprngopr  38036  brvvdif  38242  elecALTV  38245  eqrel2  38277  dmecd  38282  relcnveq2  38301  eldmxrncnvepres  38386  eldmxrncnvepres2  38387  elrelscnveq2  38474  extssr  38490  elrefrelsrel  38501  refreleq  38502  elcnvrefrelsrel  38517  elsymrelsrel  38538  symreleq  38539  eltrrelsrel  38562  trreleq  38563  eleqvrelsrel  38575  eqvreleq  38583  redundpim3  38611  erALTVeq1  38651  elfunsALTVfunALTV  38679  eldisjsdisj  38709  eldisjeq  38723  disjsuc  38741  parteq1  38756  parteq2  38757  islshpsm  38963  lcvexchlem1  39017  opcon1b  39181  isat3  39290  glbconN  39360  cdleme32fva  40420  cdlemg2cex  40574  dibelval3  41130  dib1dim  41148  doch11  41356  dochsordN  41357  mapdordlem1a  41617  mapd11  41622  mapdsord  41638  mapdcnv11N  41642  mapd0  41648  sn-iotalem  42198  ricfld  42507  fimgmcyc  42511  fsuppind  42567  mrefg2  42684  jm2.23  42973  wepwsolem  43019  dnwech  43025  islssfg2  43048  gicabl  43076  onsupmaxb  43216  onsupeqnmax  43224  orddif0suc  43245  oadif1lem  43356  oadif1  43357  fzunt  43432  fzuntd  43433  fzunt1d  43434  fzuntgd  43435  ifpbi2  43444  ifpbi3  43445  ifpbi1  43454  ifpbi12  43465  ifpbi13  43466  ontric3g  43499  pwinfig  43538  inintabd  43556  cnvcnvintabd  43577  cnvintabd  43580  intimag  43633  briunov2  43659  heeq12  43753  sbcheg  43756  uneqsn  44002  ntrneineine0lem  44060  ntrneineine1lem  44061  ntrneik2  44069  ntrneix2  44070  ntrneik13  44075  ntrneix13  44076  ralbidar  44422  rexbidar  44423  trsbc  44518  relpeq1  44922  relpeq2  44923  relpeq3  44924  relpeq4  44925  relpeq5  44926  n0abso  44954  modelaxreplem3  44958  iindif2f  45142  rnmptpr  45159  iccintsng  45508  xlimres  45806  fsetsniunop  47037  fsetsnprcnex  47043  fcoresf1ob  47061  f1cof1b  47065  f1ocof1ob  47069  dfateq12d  47114  aov0nbovbi  47183  fnotaovb  47186  ichbidv  47441  sprsymrelf  47483  prprsprreu  47507  prprreueq  47508  edgusgrclnbfin  47830  dfclnbgr6  47844  dfnbgr6  47845  isubgredg  47854  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  rngcsectALTV  48263  ringcsectALTV  48297  lindslinindsimp2lem5  48451  xpco2  48845  opndisj  48891  i0oii  48908  io1ii  48909  iscnrm3lem2  48923  uobffth  49207  uobeqw  49208  thincpropd  49431  termcpropd  49492