Theorem 3bitr4g 316

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi1d  346  pm5.32rd  580  orbi2d  912  orbi1d  913  ifpbi123d  1072  3orbi123d  1429  3anbi123d  1430  nanbi1  1488  nanbi2  1489  xorbi12d  1512  hadbi123d  1589  had0  1599  cadbi123d  1605  nfbiit  1845  nfbidv  1917  sbequ  2084  nfbidf  2219  drex1v  2382  drnf1v  2383  drex1  2457  drnf1  2459  sb4b  2493  sb4bOLD  2494  drsb1  2529  eujustALT  2651  eubi  2663  eleq1ab  2799  eqeq1d  2821  eqeq1dALT  2822  eqeq2d  2830  abbi1  2882  eleq1w  2893  eleq2w  2894  eleq1d  2895  eleq2d  2896  eleq2dALT  2897  abbi2dv  2948  nfceqdf  2970  drnfc1  2995  drnfc1OLD  2996  drnfc2  2997  neleq12d  3125  ralbidv2  3193  r19.21t  3212  ralbida  3228  rexbidv2  3293  r19.23t  3311  rexbida  3316  ralrexbid  3320  ralcom2w  3361  ralcom2  3362  reubida  3386  reubidva  3387  rmobida  3391  raleqf  3396  rexeqf  3397  reueq1f  3398  rmoeq1f  3399  reueq1  3406  rmoeq1  3407  cbvraldva2  3455  cbvrexdva2  3456  cbvrexdva2OLD  3457  dfsbcq  3772  sbceqbid  3777  sbcbid  3824  sbcbi2OLD  3830  eqsbc3r  3835  sbcrext  3854  sbcabel  3859  psseq1  4062  psseq2  4063  ssconb  4112  uneq1  4130  ineq1OLD  4180  difin2  4264  reuun2  4284  sbcnel12g  4361  sbnfc2  4386  reldisj  4400  undif4  4414  disjssun  4415  pssdifcom1  4433  pssdifcom2  4434  sbcssg  4461  eltpg  4615  raltpg  4626  rextpg  4627  r19.12sn  4648  intmin4  4896  dfiun2g  4946  dfiun2gOLD  4947  iindif1  4988  iindif2  4990  iinin2  4991  disjprgw  5052  disjprg  5053  disjxun  5055  breq  5059  breq1  5060  breq2  5061  treq  5169  reusv2lem5  5293  rexxfrd  5300  rexxfr2d  5302  rexxfrd2  5304  rabxfrd  5308  opthg2  5362  oteqex2  5380  oteqex  5381  poeq1  5470  soeq1  5487  freq1  5518  weeq1  5536  weeq2  5537  opthprc  5609  wesn  5633  releq  5644  sbcrel  5648  eqrel  5651  eqrelrel  5663  xpiindi  5699  dmopab2rex  5779  dfres3  5851  brres  5853  resieq  5857  dmsnopg  6063  dfco2a  6092  ordeq  6191  limeq  6196  ordunisssuc  6286  iotaeq  6319  sniota  6339  sbcfung  6372  imadif  6431  fneq1  6437  fneq2  6438  feq1  6488  feq2  6489  feq3  6490  sbcfng  6504  sbcfg  6505  f1eq1  6563  f1eq2  6564  f1eq3  6565  foeq1  6579  foeq2  6580  foeq3  6581  f1oeq1  6597  f1oeq2  6598  f1oeq3  6599  mpteqb  6780  rexrnmptw  6854  rexrnmpt  6856  dffo3  6861  fmptco  6884  dff13  7005  f1imaeq  7015  f1imapss  7016  cbvexfo  7038  f1eqcocnv  7049  fliftcnv  7056  isoeq1  7062  isoeq2  7063  isoeq3  7064  isoeq4  7065  isoeq5  7066  isomin  7082  isowe  7094  nfriotadw  7114  mpoeq123  7218  rexrnmpo  7282  iunpw  7485  tfinds  7566  fiun  7636  f1iun  7637  opiota  7749  ottpos  7894  dmtpos  7896  onoviun  7972  smoeq  7979  smoiso2  7998  tfr2b  8024  oarec  8180  oeeui  8220  nnacan  8246  nnmcan  8252  ereq1  8288  ereq2  8289  elecg  8324  ereldm  8329  ixpiin  8480  boxriin  8496  boxcutc  8497  omxpenlem  8610  nnsdomo  8705  enfi  8726  isfinite2  8768  ixpfi2  8814  elfi2  8870  fipwss  8885  ennum  9368  cardsdom2  9409  aleph11  9502  alephiso  9516  fin23lem26  9739  compssiso  9788  isf34lem4  9791  isfin5-2  9805  fin1a2lem5  9818  brdom7disj  9945  brdom6disj  9946  fpwwe2lem8  10051  fpwwe2lem12  10055  fpwwe2lem13  10056  genpass  10423  ltasr  10514  axpre-lttri  10579  infm3  11592  creur  11624  eqreznegel  12326  rpneg  12413  ltxr  12502  icoshftf1o  12852  elfzm11  12970  elfzomelpfzo  13133  nn0ennn  13339  nnesq  13580  hashbclem  13802  hashf1lem1  13805  leiso  13809  fz1isolem  13811  pr2pwpr  13829  repsdf2  14132  dfrtrclrec2  14408  rexfiuz  14699  cau4  14708  ello1mpt2  14871  o1lo1  14886  fsumcom2  15121  incexc2  15185  fprodcom2  15330  dvdsflip  15659  bitsmod  15777  bitscmp  15779  smueqlem  15831  divgcdcoprm0  16001  hashdvds  16104  prmreclem2  16245  vdwapun  16302  vdwmc2  16307  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  18947  gsumcom2  19087  dmdprd  19112  dprdw  19124  subgdmdprd  19148  pgpfac1lem2  19189  pgpfac1lem4  19192  ringpropd  19324  crngpropd  19325  crngunit  19404  unitpropd  19439  isnirred  19442  drngpropd  19521  fldpropd  19522  subrgpropd  19562  rhmpropd  19563  acsfn1p  19570  abvpropd  19605  lmodprop2d  19688  lsspropd  19781  lmhmpropd  19837  lbspropd  19863  lvecprop2d  19930  lvecpropd  19931  opprdomn  20066  fiidomfld  20073  assapropd  20093  psrbagconf1o  20146  mplmonmul  20237  phlpropd  20791  mat1dimbas  21073  tpspropd  21538  tgss2  21587  lmbr2  21859  ist1-2  21947  ist1-3  21949  subislly  22081  dissnlocfin  22129  iskgen3  22149  txcnmpt  22224  hausdiag  22245  hauseqlcld  22246  xkococnlem  22259  tgqtop  22312  txhmeo  22403  uffix2  22524  ufildr  22531  txflf  22606  tgphaus  22717  qustgplem  22721  qustgphaus  22723  xpsdsval  22983  blin  23023  blres  23033  xmeterval  23034  xmspropd  23075  mspropd  23076  setsms  23082  metequiv  23111  metustsym  23157  restmetu  23172  ngppropd  23238  xrtgioo  23406  metdsge  23449  icopnfcnv  23538  iccpnfcnv  23540  lmhmclm  23683  lmmbr  23853  equivcmet  23912  cmspropd  23944  iunmbl2  24150  ioombl1lem4  24154  mbfaddlem  24253  i1fmullem  24287  itg1mulc  24297  iblcnlem1  24380  iblrelem  24383  iblre  24386  iblcn  24391  limcun  24485  mvth  24581  ofmulrt  24863  resinf1o  25112  quad2  25409  1cubr  25412  dcubic  25416  wilthlem2  25638  dvdsflf1o  25756  dvdsflsumcom  25757  fsumvma  25781  vmasum  25784  logfac2  25785  logfaclbnd  25790  dchrelbas3  25806  lgsquadlem1  25948  lgsquadlem2  25949  ax5seg  26716  ushgredgedg  27003  ushgredgedgloop  27005  nbumgrvtx  27120  upgriswlk  27414  wspniunwspnon  27694  rusgrnumwwlkb0  27742  isclwwlknx  27806  clwwlknscsh  27833  clwwlknonel  27866  0trl  27893  0spth  27897  0clwlk  27901  0crct  27904  0cycl  27905  eupth2lem2  27990  eucrct2eupth  28016  fusgr2wsp2nb  28105  ocin  29065  chpsscon3  29272  chscllem2  29407  adjval  29659  pjimai  29945  mdsldmd1i  30100  elat2  30109  mdsymi  30180  sbceqbidf  30242  rmoxfrd  30249  rmounid  30251  disjxun0  30316  disjrdx  30333  eqrelrd2  30359  fmptcof2  30394  ofpreima  30402  funcnv5mpt  30405  1stpreima  30434  2ndpreima  30435  fpwrelmapffslem  30460  qsxpid  30920  smatrcl  31054  locfinreflem  31097  zhmnrg  31201  qqhval2  31216  ismntop  31260  reprsuc  31879  reprdifc  31891  bnj919  32031  bnj956  32041  bnj976  32042  bnj1366  32094  bnj916  32198  satfvsucsuc  32605  satfdm  32609  dmopab3rexdif  32645  dfpo2  32984  eqfunresadj  32997  sscoid  33367  dfrdg4  33405  altopthbg  33422  broutsideof3  33580  bj-nnfbi  34050  bj-cbvexdv  34115  bj-sbievw  34164  mobidvALT  34174  bj-restuni  34380  bj-elid6  34454  cbveud  34645  cbvreud  34646  exrecfnlem  34652  wl-sb8eut  34805  wl-sb8mot  34806  wl-clabtv  34821  wl-clabt  34822  wl-dfralf  34831  wl-dfrexf  34839  wl-dfrmof  34847  wl-dfreuf  34851  wl-dfrabf  34856  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem25  34909  ftc1anclem5  34963  istotbnd3  35041  sstotbnd  35045  heibor  35091  isass  35116  isidlc  35285  smprngopr  35322  brvvdif  35516  elecALTV  35519  eqrel2  35549  dmecd  35554  relcnveq2  35572  elrelscnveq2  35725  extssr  35741  elrefrelsrel  35751  refreleq  35752  elcnvrefrelsrel  35764  elsymrelsrel  35785  symreleq  35786  eltrrelsrel  35809  trreleq  35810  eleqvrelsrel  35821  eqvreleq  35829  redundpim3  35857  erALTVeq1  35895  elfunsALTVfunALTV  35922  eldisjsdisj  35952  eldisjeq  35966  islshpsm  36108  lcvexchlem1  36162  opcon1b  36326  isat3  36435  glbconN  36505  cdleme32fva  37565  cdlemg2cex  37719  dibelval3  38275  dib1dim  38293  doch11  38501  dochsordN  38502  mapdordlem1a  38762  mapd11  38767  mapdsord  38783  mapdcnv11N  38787  mapd0  38793  lmhmlvec  39138  mrefg2  39294  jm2.23  39583  wepwsolem  39632  dnwech  39638  islssfg2  39661  gicabl  39689  isdomn3  39794  ifpbi2  39822  ifpbi3  39823  ifpbi23  39828  ifpbi1  39833  ifpbi12  39844  ifpbi13  39845  ontric3g  39878  pwinfig  39910  inintabd  39929  cnvcnvintabd  39950  cnvintabd  39953  intimag  39991  briunov2  40017  heeq12  40112  sbcheg  40115  rcompleq  40360  uneqsn  40363  ntrneineine0lem  40423  ntrneineine1lem  40424  ntrneik2  40432  ntrneix2  40433  ntrneik13  40438  ntrneix13  40439  ralbidar  40767  rexbidar  40768  trsbc  40864  rnmptpr  41422  dffo3f  41427  iccintsng  41788  xlimres  42091  dfateq12d  43315  aov0nbovbi  43384  fnotaovb  43387  sprsymrelf  43647  prprsprreu  43671  prprreueq  43672  mgmhmpropd  44042  rngcsect  44241  rngcsectALTV  44253  ringcsect  44292  ringcsectALTV  44316  lindslinindsimp2lem5  44507