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	syl5bb 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  577  orbi2d  912  orbi1d  913  ifpbi123d  1076  ifpbi123dOLD  1077  3orbi123d  1433  3anbi123d  1434  nanbi1  1495  nanbi2  1496  xorbi12d  1521  hadbi123d  1599  had0  1609  cadbi123d  1615  nfbiit  1856  nfbidv  1928  sbequ  2089  nfbidf  2220  drex1v  2370  drnf1v  2371  drnf1vOLD  2372  drex1  2442  drnf1  2444  sb4b  2476  sb4bOLD  2477  drsb1  2500  eujustALT  2573  eubi  2585  eleq1ab  2718  eqeq1d  2741  eqeq1dALT  2742  eqeq2d  2750  abbi1  2807  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2d  2825  eleq2dALT  2826  abbi2dv  2878  nfceqdf  2903  nfceqdfOLD  2904  drnfc1  2927  drnfc1OLD  2928  drnfc2  2929  drnfc2OLD  2930  neleq12d  3054  ralbidv2  3120  r19.21t  3139  ralbidaOLD  3159  rexbidv2  3225  r19.23t  3243  rexbida  3248  ralrexbidOLD  3253  ralcom2  3290  reubida  3319  reubidva  3320  rmobida  3324  rmobidva  3325  raleqf  3330  rexeqf  3331  reueq1f  3332  rmoeq1f  3333  raleqbidvv  3336  reueq1  3342  rmoeq1  3343  cbvraldva2  3389  cbvrexdva2  3390  dfsbcq  3721  sbceqbid  3726  sbcbid  3777  sbcbi2  3782  eqsbc2  3789  sbcrext  3810  sbcabel  3815  ss2abdv  4001  psseq1  4026  psseq2  4027  ssconb  4076  uneq1  4094  difin2  4230  rcompleq  4234  reuun2  4253  sbcnel12g  4350  sbnfc2  4375  reldisj  4390  reldisjOLD  4391  undif4  4405  disjssun  4406  pssdifcom1  4425  pssdifcom2  4426  sbcssg  4459  eltpg  4626  raltpg  4639  rextpg  4640  r19.12sn  4661  intmin4  4913  dfiun2g  4965  iindif1  5008  iindif2  5010  iinin2  5011  disjprgw  5073  disjprg  5074  disjxun  5076  breq  5080  breq1  5081  breq2  5082  treq  5201  reusv2lem5  5328  rexxfrd  5335  rexxfr2d  5337  rexxfrd2  5339  rabxfrd  5343  opthg2  5396  oteqex2  5415  oteqex  5416  poeq1  5505  soeq1  5523  freq1  5558  weeq1  5576  weeq2  5577  opthprc  5650  wesn  5674  releq  5685  sbcrel  5689  eqrel  5692  eqrelrel  5704  xpiindi  5741  dmopab2rex  5823  dfres3  5893  brres  5895  resieq  5899  dmsnopg  6113  dfco2a  6147  dfpo2  6196  ordeq  6270  limeq  6275  ordunisssuc  6365  iotaeq  6401  sniota  6421  sbcfung  6454  imadif  6514  fneq1  6520  fneq2  6521  feq1  6577  feq2  6578  feq3  6579  sbcfng  6593  sbcfg  6594  f1eq1  6661  f1eq2  6662  f1eq3  6663  foeq1  6680  foeq2  6681  foeq3  6682  f1oeq1  6700  f1oeq2  6701  f1oeq3  6702  mpteqb  6888  rexrnmptw  6965  rexrnmpt  6967  dffo3  6972  fmptco  6995  dff13  7122  f1imaeq  7132  f1imapss  7133  cbvexfo  7155  f1eqcocnv  7166  f1eqcocnvOLD  7167  fliftcnv  7175  isoeq1  7181  isoeq2  7182  isoeq3  7183  isoeq4  7184  isoeq5  7185  isomin  7201  isowe  7213  nfriotadw  7233  mpoeq123  7338  rexrnmpo  7404  iunpw  7612  tfinds  7694  fiun  7772  f1iun  7773  opiota  7885  ottpos  8036  dmtpos  8038  onoviun  8158  smoeq  8165  smoiso2  8184  tfr2b  8211  oarec  8369  oeeui  8409  nnacan  8435  nnmcan  8441  ereq1  8479  ereq2  8480  elecg  8515  ereldm  8520  ixpiin  8686  boxriin  8702  boxcutc  8703  omxpenlem  8829  enfiALT  8939  nnsdomo  8980  isfinite2  9033  ixpfi2  9078  elfi2  9134  fipwss  9149  ttrclse  9446  ennum  9689  cardsdom2  9730  aleph11  9824  alephiso  9838  fin23lem26  10065  compssiso  10114  isf34lem4  10117  isfin5-2  10131  fin1a2lem5  10144  brdom7disj  10271  brdom6disj  10272  fpwwe2lem7  10377  fpwwe2lem11  10381  fpwwe2lem12  10382  genpass  10749  ltasr  10840  axpre-lttri  10905  infm3  11917  creur  11950  eqreznegel  12656  rpneg  12744  ltxr  12833  icoshftf1o  13188  elfzm11  13309  elfzomelpfzo  13472  nn0ennn  13680  nnesq  13923  hashbclem  14145  hashf1lem1  14149  hashf1lem1OLD  14150  leiso  14154  fz1isolem  14156  pr2pwpr  14174  repsdf2  14472  dfrtrclrec2  14750  rexfiuz  15040  cau4  15049  ello1mpt2  15212  o1lo1  15227  fsumcom2  15467  incexc2  15531  fprodcom2  15675  dvdsflip  16007  bitsmod  16124  bitscmp  16126  smueqlem  16178  divgcdcoprm0  16351  hashdvds  16457  prmreclem2  16599  vdwapun  16656  vdwmc2  16661  imasaddfnlem  17220  comfeq  17396  oppcsect  17471  funcres2b  17593  funcpropd  17597  fullpropd  17617  fthpropd  17618  fthres2b  17627  fthres2c  17628  fullres2c  17636  ffthres2c  17637  fucsect  17671  fucinv  17672  setcsect  17785  pospropd  18026  tosso  18118  odulatb  18133  oduclatb  18206  odudlatb  18224  isipodrs  18236  issgrpv  18358  issgrpn0  18359  mndpropd  18391  mhmpropd  18417  issubm2  18424  efmnd1bas  18513  grppropd  18575  grpinvcnv  18624  conjghm  18846  conjnmzb  18850  ghmpropd  18853  gapm  18893  symg1bas  18979  pmtrfrn  19047  cmnpropd  19377  ablpropd  19378  eqgabl  19417  gsumcom2  19557  dmdprd  19582  dprdw  19594  subgdmdprd  19618  pgpfac1lem2  19659  pgpfac1lem4  19662  ringpropd  19802  crngpropd  19803  crngunit  19885  unitpropd  19920  isnirred  19923  drngpropd  19999  fldpropd  20000  subrgpropd  20040  rhmpropd  20041  acsfn1p  20048  abvpropd  20083  lmodprop2d  20166  lsspropd  20260  lmhmpropd  20316  lbspropd  20342  lvecprop2d  20409  lvecpropd  20410  opprdomn  20553  fiidomfld  20561  phlpropd  20841  assapropd  21057  psrbagconf1o  21120  psrbagconf1oOLD  21121  mplmonmul  21218  ismhp3  21314  mat1dimbas  21602  tpspropd  22068  tgss2  22118  lmbr2  22391  ist1-2  22479  ist1-3  22481  subislly  22613  dissnlocfin  22661  iskgen3  22681  txcnmpt  22756  hausdiag  22777  hauseqlcld  22778  xkococnlem  22791  tgqtop  22844  txhmeo  22935  uffix2  23056  ufildr  23063  txflf  23138  tgphaus  23249  qustgplem  23253  qustgphaus  23255  xpsdsval  23515  blin  23555  blres  23565  xmeterval  23566  xmspropd  23607  mspropd  23608  setsms  23616  metequiv  23646  metustsym  23692  restmetu  23707  ngppropd  23774  xrtgioo  23950  metdsge  23993  icopnfcnv  24086  iccpnfcnv  24088  lmhmclm  24231  lmmbr  24403  equivcmet  24462  cmspropd  24494  iunmbl2  24702  ioombl1lem4  24706  mbfaddlem  24805  i1fmullem  24839  itg1mulc  24850  iblcnlem1  24933  iblrelem  24936  iblre  24939  iblcn  24944  limcun  25040  mvth  25137  ofmulrt  25423  resinf1o  25673  quad2  25970  1cubr  25973  dcubic  25977  wilthlem2  26199  dvdsflf1o  26317  dvdsflsumcom  26318  fsumvma  26342  vmasum  26345  logfac2  26346  logfaclbnd  26351  dchrelbas3  26367  lgsquadlem1  26509  lgsquadlem2  26510  ax5seg  27287  ushgredgedg  27577  ushgredgedgloop  27579  nbumgrvtx  27694  upgriswlk  27988  wspniunwspnon  28267  rusgrnumwwlkb0  28315  isclwwlknx  28379  clwwlknscsh  28405  clwwlknonel  28438  0trl  28465  0spth  28469  0clwlk  28473  0crct  28476  0cycl  28477  eupth2lem2  28562  eucrct2eupth  28588  fusgr2wsp2nb  28677  ocin  29637  chpsscon3  29844  chscllem2  29979  adjval  30231  pjimai  30517  mdsldmd1i  30672  elat2  30681  mdsymi  30752  sbceqbidf  30814  rmoxfrd  30820  rmounid  30822  disjxun0  30892  disjrdx  30909  eqrelrd2  30935  fmptcof2  30973  ofpreima  30981  funcnv5mpt  30984  ressupprn  31003  1stpreima  31018  2ndpreima  31019  fpwrelmapffslem  31046  qsxpid  31537  grplsm0l  31570  smatrcl  31725  locfinreflem  31769  zarcls  31803  zhmnrg  31896  qqhval2  31911  ismntop  31955  reprsuc  32574  reprdifc  32586  bnj919  32726  bnj956  32735  bnj976  32736  bnj1366  32788  bnj916  32892  satfvsucsuc  33306  satfdm  33310  dmopab3rexdif  33346  imaeqsalv  33670  eqfunresadj  33714  xpord3pred  33777  eqscut2  33979  sscoid  34194  dfrdg4  34232  altopthbg  34249  broutsideof3  34407  bj-nnfbi  34886  bj-cbvexdv  34961  bj-sbievw  35010  mobidvALT  35020  bj-restuni  35247  bj-elid6  35320  cbveud  35522  cbvreud  35523  exrecfnlem  35529  wl-ifp-ncond2  35615  wl-ifpimpr  35616  wl-3xorbi123d  35625  wl-sb8eut  35711  wl-sb8mot  35712  wl-clabtv  35727  wl-clabt  35728  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem25  35781  ftc1anclem5  35833  istotbnd3  35908  sstotbnd  35912  heibor  35958  isass  35983  isidlc  36152  smprngopr  36189  brvvdif  36381  elecALTV  36384  eqrel2  36414  dmecd  36419  relcnveq2  36437  elrelscnveq2  36590  extssr  36606  elrefrelsrel  36616  refreleq  36617  elcnvrefrelsrel  36629  elsymrelsrel  36650  symreleq  36651  eltrrelsrel  36674  trreleq  36675  eleqvrelsrel  36686  eqvreleq  36694  redundpim3  36722  erALTVeq1  36760  elfunsALTVfunALTV  36787  eldisjsdisj  36817  eldisjeq  36831  islshpsm  36973  lcvexchlem1  37027  opcon1b  37191  isat3  37300  glbconN  37370  cdleme32fva  38430  cdlemg2cex  38584  dibelval3  39140  dib1dim  39158  doch11  39366  dochsordN  39367  mapdordlem1a  39627  mapd11  39632  mapdsord  39648  mapdcnv11N  39652  mapd0  39658  sn-iotalem  40169  lmhmlvec  40241  fsuppind  40259  mrefg2  40509  jm2.23  40798  wepwsolem  40847  dnwech  40853  islssfg2  40876  gicabl  40904  isdomn3  41009  ifpbi2  41036  ifpbi3  41037  ifpbi23  41042  ifpbi1  41046  ifpbi12  41057  ifpbi13  41058  ontric3g  41091  pwinfig  41121  inintabd  41140  cnvcnvintabd  41161  cnvintabd  41164  intimag  41217  briunov2  41243  heeq12  41337  sbcheg  41340  uneqsn  41586  ntrneineine0lem  41646  ntrneineine1lem  41647  ntrneik2  41655  ntrneix2  41656  ntrneik13  41661  ntrneix13  41662  ralbidar  42016  rexbidar  42017  trsbc  42113  rnmptpr  42666  dffo3f  42670  iccintsng  43015  xlimres  43316  fsetsniunop  44494  fsetsnprcnex  44500  fcoresf1ob  44518  f1cof1b  44520  f1ocof1ob  44524  dfateq12d  44569  aov0nbovbi  44638  fnotaovb  44641  ichbidv  44857  sprsymrelf  44899  prprsprreu  44923  prprreueq  44924  mgmhmpropd  45291  rngcsect  45490  rngcsectALTV  45502  ringcsect  45541  ringcsectALTV  45565  lindslinindsimp2lem5  45755  opndisj  46148  i0oii  46165  io1ii  46166  iscnrm3lem2  46180