Theorem 3bitr4g 317

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi1d  347  pm5.32rd  581  orbi2d  913  orbi1d  914  ifpbi123d  1075  ifpbi123dOLD  1076  3orbi123d  1432  3anbi123d  1433  nanbi1  1492  nanbi2  1493  xorbi12d  1518  hadbi123d  1596  had0  1606  cadbi123d  1612  nfbiit  1852  nfbidv  1923  sbequ  2088  nfbidf  2224  drex1v  2377  drnf1v  2378  drex1  2452  drnf1  2454  sb4b  2488  sb4bOLD  2489  drsb1  2513  eujustALT  2632  eubi  2644  eleq1ab  2778  eqeq1d  2800  eqeq1dALT  2801  eqeq2d  2809  abbi1  2861  eleq1w  2872  eleq2w  2873  eleq1d  2874  eleq2d  2875  eleq2dALT  2876  abbi2dv  2927  nfceqdf  2951  drnfc1  2974  drnfc2  2975  neleq12d  3095  ralbidv2  3160  r19.21t  3178  ralbida  3194  rexbidv2  3254  r19.23t  3272  rexbida  3277  ralrexbid  3281  ralcom2  3316  reubida  3340  reubidva  3341  rmobida  3345  raleqf  3350  rexeqf  3351  reueq1f  3352  rmoeq1f  3353  reueq1  3360  rmoeq1  3361  cbvraldva2  3403  cbvrexdva2  3404  cbvrexdva2OLD  3405  dfsbcq  3722  sbceqbid  3727  sbcbid  3773  sbcbi2  3778  eqsbc3r  3784  sbcrext  3802  sbcabel  3807  ss2abdv  3991  psseq1  4015  psseq2  4016  ssconb  4065  uneq1  4083  ineq1OLD  4132  difin2  4216  rcompleq  4220  reuun2  4238  sbcnel12g  4319  sbnfc2  4344  reldisj  4359  reldisjOLD  4360  undif4  4374  disjssun  4375  pssdifcom1  4393  pssdifcom2  4394  sbcssg  4421  eltpg  4583  raltpg  4594  rextpg  4595  r19.12sn  4616  intmin4  4867  dfiun2g  4917  dfiun2gOLD  4918  iindif1  4960  iindif2  4962  iinin2  4963  disjprgw  5025  disjprg  5026  disjxun  5028  breq  5032  breq1  5033  breq2  5034  treq  5142  reusv2lem5  5268  rexxfrd  5275  rexxfr2d  5277  rexxfrd2  5279  rabxfrd  5283  opthg2  5336  oteqex2  5354  oteqex  5355  poeq1  5441  soeq1  5458  freq1  5489  weeq1  5507  weeq2  5508  opthprc  5580  wesn  5604  releq  5615  sbcrel  5619  eqrel  5622  eqrelrel  5634  xpiindi  5670  dmopab2rex  5750  dfres3  5823  brres  5825  resieq  5829  dmsnopg  6037  dfco2a  6066  ordeq  6166  limeq  6171  ordunisssuc  6261  iotaeq  6295  sniota  6315  sbcfung  6348  imadif  6408  fneq1  6414  fneq2  6415  feq1  6468  feq2  6469  feq3  6470  sbcfng  6484  sbcfg  6485  f1eq1  6544  f1eq2  6545  f1eq3  6546  foeq1  6561  foeq2  6562  foeq3  6563  f1oeq1  6579  f1oeq2  6580  f1oeq3  6581  mpteqb  6764  rexrnmptw  6838  rexrnmpt  6840  dffo3  6845  fmptco  6868  dff13  6991  f1imaeq  7001  f1imapss  7002  cbvexfo  7024  f1eqcocnv  7035  f1eqcocnvOLD  7036  fliftcnv  7043  isoeq1  7049  isoeq2  7050  isoeq3  7051  isoeq4  7052  isoeq5  7053  isomin  7069  isowe  7081  nfriotadw  7101  mpoeq123  7205  rexrnmpo  7269  iunpw  7473  tfinds  7554  fiun  7626  f1iun  7627  opiota  7739  ottpos  7885  dmtpos  7887  onoviun  7963  smoeq  7970  smoiso2  7989  tfr2b  8015  oarec  8171  oeeui  8211  nnacan  8237  nnmcan  8243  ereq1  8279  ereq2  8280  elecg  8315  ereldm  8320  ixpiin  8471  boxriin  8487  boxcutc  8488  omxpenlem  8601  nnsdomo  8698  enfi  8718  isfinite2  8760  ixpfi2  8806  elfi2  8862  fipwss  8877  ennum  9360  cardsdom2  9401  aleph11  9495  alephiso  9509  fin23lem26  9736  compssiso  9785  isf34lem4  9788  isfin5-2  9802  fin1a2lem5  9815  brdom7disj  9942  brdom6disj  9943  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  genpass  10420  ltasr  10511  axpre-lttri  10576  infm3  11587  creur  11619  eqreznegel  12322  rpneg  12409  ltxr  12498  icoshftf1o  12852  elfzm11  12973  elfzomelpfzo  13136  nn0ennn  13342  nnesq  13584  hashbclem  13806  hashf1lem1  13809  leiso  13813  fz1isolem  13815  pr2pwpr  13833  repsdf2  14131  dfrtrclrec2  14409  rexfiuz  14699  cau4  14708  ello1mpt2  14871  o1lo1  14886  fsumcom2  15121  incexc2  15185  fprodcom2  15330  dvdsflip  15659  bitsmod  15775  bitscmp  15777  smueqlem  15829  divgcdcoprm0  15999  hashdvds  16102  prmreclem2  16243  vdwapun  16300  vdwmc2  16305  imasaddfnlem  16793  comfeq  16968  oppcsect  17040  funcres2b  17159  funcpropd  17162  fullpropd  17182  fthpropd  17183  fthres2b  17192  fthres2c  17193  fullres2c  17201  ffthres2c  17202  fucsect  17234  fucinv  17235  setcsect  17341  tosso  17638  pospropd  17736  odulatb  17745  oduclatb  17746  isipodrs  17763  odudlatb  17798  issgrpv  17895  issgrpn0  17896  mndpropd  17928  mhmpropd  17954  issubm2  17961  efmnd1bas  18050  grppropd  18110  grpinvcnv  18159  conjghm  18381  conjnmzb  18385  ghmpropd  18388  gapm  18428  symg1bas  18511  pmtrfrn  18578  cmnpropd  18908  ablpropd  18909  eqgabl  18948  gsumcom2  19088  dmdprd  19113  dprdw  19125  subgdmdprd  19149  pgpfac1lem2  19190  pgpfac1lem4  19193  ringpropd  19328  crngpropd  19329  crngunit  19408  unitpropd  19443  isnirred  19446  drngpropd  19522  fldpropd  19523  subrgpropd  19563  rhmpropd  19564  acsfn1p  19571  abvpropd  19606  lmodprop2d  19689  lsspropd  19782  lmhmpropd  19838  lbspropd  19864  lvecprop2d  19931  lvecpropd  19932  opprdomn  20067  fiidomfld  20074  phlpropd  20344  assapropd  20558  psrbagconf1o  20612  mplmonmul  20704  mat1dimbas  21077  tpspropd  21543  tgss2  21592  lmbr2  21864  ist1-2  21952  ist1-3  21954  subislly  22086  dissnlocfin  22134  iskgen3  22154  txcnmpt  22229  hausdiag  22250  hauseqlcld  22251  xkococnlem  22264  tgqtop  22317  txhmeo  22408  uffix2  22529  ufildr  22536  txflf  22611  tgphaus  22722  qustgplem  22726  qustgphaus  22728  xpsdsval  22988  blin  23028  blres  23038  xmeterval  23039  xmspropd  23080  mspropd  23081  setsms  23087  metequiv  23116  metustsym  23162  restmetu  23177  ngppropd  23243  xrtgioo  23411  metdsge  23454  icopnfcnv  23547  iccpnfcnv  23549  lmhmclm  23692  lmmbr  23862  equivcmet  23921  cmspropd  23953  iunmbl2  24161  ioombl1lem4  24165  mbfaddlem  24264  i1fmullem  24298  itg1mulc  24308  iblcnlem1  24391  iblrelem  24394  iblre  24397  iblcn  24402  limcun  24498  mvth  24595  ofmulrt  24878  resinf1o  25128  quad2  25425  1cubr  25428  dcubic  25432  wilthlem2  25654  dvdsflf1o  25772  dvdsflsumcom  25773  fsumvma  25797  vmasum  25800  logfac2  25801  logfaclbnd  25806  dchrelbas3  25822  lgsquadlem1  25964  lgsquadlem2  25965  ax5seg  26732  ushgredgedg  27019  ushgredgedgloop  27021  nbumgrvtx  27136  upgriswlk  27430  wspniunwspnon  27709  rusgrnumwwlkb0  27757  isclwwlknx  27821  clwwlknscsh  27847  clwwlknonel  27880  0trl  27907  0spth  27911  0clwlk  27915  0crct  27918  0cycl  27919  eupth2lem2  28004  eucrct2eupth  28030  fusgr2wsp2nb  28119  ocin  29079  chpsscon3  29286  chscllem2  29421  adjval  29673  pjimai  29959  mdsldmd1i  30114  elat2  30123  mdsymi  30194  sbceqbidf  30257  rmoxfrd  30264  rmounid  30266  disjxun0  30337  disjrdx  30354  eqrelrd2  30380  fmptcof2  30420  ofpreima  30428  funcnv5mpt  30431  ressupprn  30450  1stpreima  30466  2ndpreima  30467  fpwrelmapffslem  30494  qsxpid  30978  smatrcl  31149  locfinreflem  31193  zarcls  31227  zhmnrg  31318  qqhval2  31333  ismntop  31377  reprsuc  31996  reprdifc  32008  bnj919  32148  bnj956  32158  bnj976  32159  bnj1366  32211  bnj916  32315  satfvsucsuc  32725  satfdm  32729  dmopab3rexdif  32765  dfpo2  33104  eqfunresadj  33117  sscoid  33487  dfrdg4  33525  altopthbg  33542  broutsideof3  33700  bj-nnfbi  34172  bj-cbvexdv  34237  bj-sbievw  34286  mobidvALT  34296  bj-restuni  34512  bj-elid6  34585  cbveud  34789  cbvreud  34790  exrecfnlem  34796  wl-ifp-ncond2  34882  wl-ifpimpr  34883  wl-3xorbi123d  34892  wl-sb8eut  34978  wl-sb8mot  34979  wl-clabtv  34994  wl-clabt  34995  wl-dfralf  35004  wl-dfrexf  35012  wl-dfrmof  35020  wl-dfreuf  35024  wl-dfrabf  35029  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem25  35082  ftc1anclem5  35134  istotbnd3  35209  sstotbnd  35213  heibor  35259  isass  35284  isidlc  35453  smprngopr  35490  brvvdif  35684  elecALTV  35687  eqrel2  35717  dmecd  35722  relcnveq2  35740  elrelscnveq2  35893  extssr  35909  elrefrelsrel  35919  refreleq  35920  elcnvrefrelsrel  35932  elsymrelsrel  35953  symreleq  35954  eltrrelsrel  35977  trreleq  35978  eleqvrelsrel  35989  eqvreleq  35997  redundpim3  36025  erALTVeq1  36063  elfunsALTVfunALTV  36090  eldisjsdisj  36120  eldisjeq  36134  islshpsm  36276  lcvexchlem1  36330  opcon1b  36494  isat3  36603  glbconN  36673  cdleme32fva  37733  cdlemg2cex  37887  dibelval3  38443  dib1dim  38461  doch11  38669  dochsordN  38670  mapdordlem1a  38930  mapd11  38935  mapdsord  38951  mapdcnv11N  38955  mapd0  38961  lmhmlvec  39452  fsuppind  39456  mrefg2  39648  jm2.23  39937  wepwsolem  39986  dnwech  39992  islssfg2  40015  gicabl  40043  isdomn3  40148  ifpbi2  40175  ifpbi3  40176  ifpbi23  40181  ifpbi1  40185  ifpbi12  40196  ifpbi13  40197  ontric3g  40230  pwinfig  40260  inintabd  40279  cnvcnvintabd  40300  cnvintabd  40303  intimag  40357  briunov2  40383  heeq12  40477  sbcheg  40480  uneqsn  40726  ntrneineine0lem  40786  ntrneineine1lem  40787  ntrneik2  40795  ntrneix2  40796  ntrneik13  40801  ntrneix13  40802  ralbidar  41149  rexbidar  41150  trsbc  41246  rnmptpr  41801  dffo3f  41806  iccintsng  42160  xlimres  42463  dfateq12d  43682  aov0nbovbi  43751  fnotaovb  43754  ichbidv  43970  sprsymrelf  44012  prprsprreu  44036  prprreueq  44037  mgmhmpropd  44405  rngcsect  44604  rngcsectALTV  44616  ringcsect  44655  ringcsectALTV  44679  lindslinindsimp2lem5  44871