Theorem 3bitr4g 313

Description: More general version of 3bitr4i 302. 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 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 288	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ 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:  bibi1d  343  pm5.32rd  578  orbi2d  914  orbi1d  915  ifpbi123d  1078  ifpbi123dOLD  1079  3orbi123d  1435  3anbi123d  1436  nanbi1  1499  nanbi2  1500  xorbi12d  1525  hadbi123d  1596  had0  1605  cadbi123d  1611  nfbiit  1853  nfbidv  1925  sbequ  2086  nfbidf  2217  drex1v  2368  drnf1v  2369  drnf1vOLD  2370  drex1  2440  drnf1  2442  sb4b  2474  drsb1  2494  eujustALT  2566  eubi  2578  eleq1ab  2711  eqeq1d  2734  eqeq1dALT  2735  eqeq2d  2743  abbi  2800  eleq1w  2816  eleq2w  2817  eleq1d  2818  eleq2d  2819  eleq2dALT  2820  eqabdv  2867  nfceqdf  2898  nfceqdfOLD  2899  drnfc1  2922  drnfc1OLD  2923  drnfc2  2924  drnfc2OLD  2925  neleq12d  3051  ralrexbidOLD  3107  ralbidv2  3173  rexbidv2  3174  r19.21t  3250  r19.23t  3252  ralbidaOLD  3268  rexbida  3269  rexeq  3321  raleqbidvvOLD  3330  cbvraldva2  3344  cbvrexdva2OLD  3346  raleqf  3349  rexeqfOLD  3351  ralcom2  3373  rmobidva  3391  reubidva  3392  rmobida  3402  reubida  3403  rmoeq1  3414  reueq1  3415  rmoeq1OLD  3416  reueq1OLD  3417  rmoeq1f  3420  reueq1f  3421  dfsbcq  3778  sbceqbid  3783  sbcbid  3834  sbcbi2  3838  eqsbc2  3845  sbcrext  3866  sbcabel  3871  ss2abdv  4059  psseq1  4086  psseq2  4087  ssconb  4136  uneq1  4155  difin2  4290  rcompleq  4294  reuun2  4313  sbcnel12g  4410  sbnfc2  4435  reldisj  4450  reldisjOLD  4451  undif4  4465  disjssun  4466  pssdifcom1  4488  pssdifcom2  4489  sbcssg  4522  eltpg  4688  raltpg  4701  rextpg  4702  r19.12sn  4723  intmin4  4980  dfiun2g  5032  dfiun2gOLD  5033  iindif1  5077  iindif2  5079  iinin2  5080  disjprgw  5142  disjprg  5143  disjxun  5145  breq  5149  breq1  5150  breq2  5151  treq  5272  reusv2lem5  5399  rexxfrd  5406  rexxfr2d  5408  rexxfrd2  5410  rabxfrd  5414  opthg2  5478  oteqex2  5498  oteqex  5499  poeq1  5590  soeq1  5608  freq1  5645  weeq1  5663  weeq2  5664  opthprc  5738  wesn  5762  releq  5774  sbcrel  5778  eqrel  5782  eqrelrel  5795  xpiindi  5833  dmopab2rex  5915  dfres3  5984  brres  5986  resieq  5990  dmsnopg  6209  dfco2a  6242  dfpo2  6292  ordeq  6368  limeq  6373  ordunisssuc  6467  iotaeq  6505  sniota  6531  sbcfung  6569  imadif  6629  fneq1  6637  fneq2  6638  feq1  6695  feq2  6696  feq3  6697  sbcfng  6711  sbcfg  6712  f1eq1  6779  f1eq2  6780  f1eq3  6781  foeq1  6798  foeq2  6799  foeq3  6800  f1oeq1  6818  f1oeq2  6819  f1oeq3  6820  mpteqb  7014  rexrnmptw  7093  rexrnmpt  7095  dffo3  7100  fmptco  7123  dff13  7250  f1imaeq  7260  f1imapss  7261  cbvexfo  7284  f1eqcocnv  7295  f1eqcocnvOLD  7296  fliftcnv  7304  isoeq1  7310  isoeq2  7311  isoeq3  7312  isoeq4  7313  isoeq5  7314  isomin  7330  isowe  7342  eqfunresadj  7353  imaeqsalv  7357  nfriotadw  7369  mpoeq123  7477  rexrnmpo  7544  iunpw  7754  tfinds  7845  fiun  7925  f1iun  7926  opiota  8041  xpord3pred  8134  ottpos  8217  dmtpos  8219  onoviun  8339  smoeq  8346  smoiso2  8365  tfr2b  8392  oarec  8558  oeeui  8598  nnacan  8624  nnmcan  8630  ereq1  8706  ereq2  8707  elecg  8742  ereldm  8747  ixpiin  8914  boxriin  8930  boxcutc  8931  omxpenlem  9069  enfiALT  9187  nnsdomo  9230  isfinite2  9297  ixpfi2  9346  elfi2  9405  fipwss  9420  ttrclse  9718  ennum  9938  cardsdom2  9979  aleph11  10075  alephiso  10089  fin23lem26  10316  compssiso  10365  isf34lem4  10368  isfin5-2  10382  fin1a2lem5  10395  brdom7disj  10522  brdom6disj  10523  fpwwe2lem7  10628  fpwwe2lem11  10632  fpwwe2lem12  10633  genpass  11000  ltasr  11091  axpre-lttri  11156  infm3  12169  creur  12202  eqreznegel  12914  rpneg  13002  ltxr  13091  icoshftf1o  13447  elfzm11  13568  elfzomelpfzo  13732  nn0ennn  13940  nnesq  14186  hashbclem  14407  hashf1lem1  14411  hashf1lem1OLD  14412  leiso  14416  fz1isolem  14418  pr2pwpr  14436  repsdf2  14724  dfrtrclrec2  15001  rexfiuz  15290  cau4  15299  ello1mpt2  15462  o1lo1  15477  fsumcom2  15716  incexc2  15780  fprodcom2  15924  dvdsflip  16256  bitsmod  16373  bitscmp  16375  smueqlem  16427  divgcdcoprm0  16598  hashdvds  16704  prmreclem2  16846  vdwapun  16903  vdwmc2  16908  imasaddfnlem  17470  comfeq  17646  oppcsect  17721  funcres2b  17843  funcpropd  17847  fullpropd  17867  fthpropd  17868  fthres2b  17877  fthres2c  17878  fullres2c  17886  ffthres2c  17887  fucsect  17921  fucinv  17922  setcsect  18035  pospropd  18276  tosso  18368  odulatb  18383  oduclatb  18456  odudlatb  18474  isipodrs  18486  issgrpv  18608  issgrpn0  18609  mndpropd  18646  mhmpropd  18674  issubm2  18681  efmnd1bas  18770  grppropd  18833  grpinvcnv  18887  conjghm  19117  conjnmzb  19121  ghmpropd  19124  gapm  19164  symg1bas  19252  pmtrfrn  19320  cmnpropd  19653  ablpropd  19654  eqgabl  19696  gsumcom2  19837  dmdprd  19862  dprdw  19874  subgdmdprd  19898  pgpfac1lem2  19939  pgpfac1lem4  19942  ringpropd  20095  crngpropd  20096  crngunit  20184  unitpropd  20223  isnirred  20226  drngpropd  20344  fldpropd  20345  resrhm2b  20386  subrgpropd  20392  rhmpropd  20393  acsfn1p  20407  abvpropd  20442  lmodprop2d  20526  lsspropd  20620  lmhmpropd  20676  lbspropd  20702  lmhmlvec  20712  lvecprop2d  20771  lvecpropd  20772  opprdomn  20911  fiidomfld  20919  phlpropd  21199  assapropd  21417  psrbagconf1o  21480  psrbagconf1oOLD  21481  mplmonmul  21582  ismhp3  21677  mat1dimbas  21965  tpspropd  22431  tgss2  22481  lmbr2  22754  ist1-2  22842  ist1-3  22844  subislly  22976  dissnlocfin  23024  iskgen3  23044  txcnmpt  23119  hausdiag  23140  hauseqlcld  23141  xkococnlem  23154  tgqtop  23207  txhmeo  23298  uffix2  23419  ufildr  23426  txflf  23501  tgphaus  23612  qustgplem  23616  qustgphaus  23618  xpsdsval  23878  blin  23918  blres  23928  xmeterval  23929  xmspropd  23970  mspropd  23971  setsms  23979  metequiv  24009  metustsym  24055  restmetu  24070  ngppropd  24137  xrtgioo  24313  metdsge  24356  icopnfcnv  24449  iccpnfcnv  24451  lmhmclm  24594  lmmbr  24766  equivcmet  24825  cmspropd  24857  iunmbl2  25065  ioombl1lem4  25069  mbfaddlem  25168  i1fmullem  25202  itg1mulc  25213  iblcnlem1  25296  iblrelem  25299  iblre  25302  iblcn  25307  limcun  25403  mvth  25500  ofmulrt  25786  resinf1o  26036  quad2  26333  1cubr  26336  dcubic  26340  wilthlem2  26562  dvdsflf1o  26680  dvdsflsumcom  26681  fsumvma  26705  vmasum  26708  logfac2  26709  logfaclbnd  26714  dchrelbas3  26730  lgsquadlem1  26872  lgsquadlem2  26873  eqscut2  27296  mulsrid  27558  ax5seg  28185  ushgredgedg  28475  ushgredgedgloop  28477  nbumgrvtx  28592  upgriswlk  28887  wspniunwspnon  29166  rusgrnumwwlkb0  29214  isclwwlknx  29278  clwwlknscsh  29304  clwwlknonel  29337  0trl  29364  0spth  29368  0clwlk  29372  0crct  29375  0cycl  29376  eupth2lem2  29461  eucrct2eupth  29487  fusgr2wsp2nb  29576  ocin  30536  chpsscon3  30743  chscllem2  30878  adjval  31130  pjimai  31416  mdsldmd1i  31571  elat2  31580  mdsymi  31651  sbceqbidf  31714  rmoxfrd  31720  rmounid  31722  disjxun0  31792  disjrdx  31809  eqrelrd2  31832  fmptcof2  31869  ofpreima  31877  funcnv5mpt  31880  ressupprn  31899  1stpreima  31915  2ndpreima  31916  fpwrelmapffslem  31944  qsxpid  32462  grplsm0l  32501  opprlidlabs  32587  ressply1mon1p  32645  smatrcl  32764  locfinreflem  32808  zarcls  32842  zhmnrg  32935  qqhval2  32950  ismntop  32994  reprsuc  33615  reprdifc  33627  bnj919  33766  bnj956  33775  bnj976  33776  bnj1366  33828  bnj916  33932  satfvsucsuc  34344  satfdm  34348  dmopab3rexdif  34384  sscoid  34873  dfrdg4  34911  altopthbg  34928  broutsideof3  35086  bj-nnfbi  35591  bj-cbvexdv  35666  bj-sbievw  35714  mobidvALT  35724  bj-restuni  35966  bj-elid6  36039  cbveud  36241  cbvreud  36242  exrecfnlem  36248  wl-ifp-ncond2  36334  wl-ifpimpr  36335  wl-3xorbi123d  36344  wl-sb8eut  36430  wl-sb8mot  36431  wl-clabtv  36447  wl-clabt  36448  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  poimirlem25  36501  ftc1anclem5  36553  istotbnd3  36627  sstotbnd  36631  heibor  36677  isass  36702  isidlc  36871  smprngopr  36908  brvvdif  37119  elecALTV  37122  eqrel2  37156  dmecd  37161  relcnveq2  37180  elrelscnveq2  37351  extssr  37367  elrefrelsrel  37378  refreleq  37379  elcnvrefrelsrel  37394  elsymrelsrel  37415  symreleq  37416  eltrrelsrel  37439  trreleq  37440  eleqvrelsrel  37452  eqvreleq  37460  redundpim3  37488  erALTVeq1  37527  elfunsALTVfunALTV  37555  eldisjsdisj  37585  eldisjeq  37599  disjsuc  37617  parteq1  37632  parteq2  37633  islshpsm  37838  lcvexchlem1  37892  opcon1b  38056  isat3  38165  glbconN  38235  glbconNOLD  38236  cdleme32fva  39296  cdlemg2cex  39450  dibelval3  40006  dib1dim  40024  doch11  40232  dochsordN  40233  mapdordlem1a  40493  mapd11  40498  mapdsord  40514  mapdcnv11N  40518  mapd0  40524  sn-iotalem  41034  ricfld  41102  fsuppind  41159  mrefg2  41430  jm2.23  41720  wepwsolem  41769  dnwech  41775  islssfg2  41798  gicabl  41826  isdomn3  41931  onsupmaxb  41973  onsupeqnmax  41981  orddif0suc  42003  oadif1lem  42114  oadif1  42115  fzunt  42191  fzuntd  42192  fzunt1d  42193  fzuntgd  42194  ifpbi2  42203  ifpbi3  42204  ifpbi1  42213  ifpbi12  42224  ifpbi13  42225  ontric3g  42258  pwinfig  42297  inintabd  42315  cnvcnvintabd  42336  cnvintabd  42339  intimag  42392  briunov2  42418  heeq12  42512  sbcheg  42515  uneqsn  42761  ntrneineine0lem  42819  ntrneineine1lem  42820  ntrneik2  42828  ntrneix2  42829  ntrneik13  42834  ntrneix13  42835  ralbidar  43189  rexbidar  43190  trsbc  43286  iindif2f  43839  rnmptpr  43858  dffo3f  43862  iccintsng  44222  xlimres  44523  fsetsniunop  45745  fsetsnprcnex  45751  fcoresf1ob  45769  f1cof1b  45771  f1ocof1ob  45775  dfateq12d  45820  aov0nbovbi  45889  fnotaovb  45892  ichbidv  46107  sprsymrelf  46149  prprsprreu  46173  prprreueq  46174  mgmhmpropd  46541  rngpropd  46659  issubrng  46710  subrngpropd  46731  rngcsect  46831  rngcsectALTV  46843  ringcsect  46882  ringcsectALTV  46906  lindslinindsimp2lem5  47096  opndisj  47488  i0oii  47505  io1ii  47506  iscnrm3lem2  47520