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 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  913  orbi1d  914  ifpbi123d  1077  ifpbi123dOLD  1078  3orbi123d  1434  3anbi123d  1435  nanbi1  1498  nanbi2  1499  xorbi12d  1524  hadbi123d  1595  had0  1604  cadbi123d  1610  nfbiit  1852  nfbidv  1924  sbequ  2085  nfbidf  2216  drex1v  2367  drnf1v  2368  drnf1vOLD  2369  drex1  2439  drnf1  2441  sb4b  2473  drsb1  2493  eujustALT  2565  eubi  2577  eleq1ab  2710  eqeq1d  2733  eqeq1dALT  2734  eqeq2d  2742  abbi  2799  eleq1w  2815  eleq2w  2816  eleq1d  2817  eleq2d  2818  eleq2dALT  2819  eqabdv  2866  nfceqdf  2897  nfceqdfOLD  2898  drnfc1  2921  drnfc1OLD  2922  drnfc2  2923  drnfc2OLD  2924  neleq12d  3050  ralrexbidOLD  3106  ralbidv2  3172  rexbidv2  3173  r19.21t  3249  r19.23t  3251  ralbidaOLD  3267  rexbida  3268  rexeq  3320  raleqbidvvOLD  3329  cbvraldva2  3343  cbvrexdva2OLD  3345  raleqf  3348  rexeqfOLD  3350  ralcom2  3372  rmobidva  3390  reubidva  3391  rmobida  3401  reubida  3402  rmoeq1  3413  reueq1  3414  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3419  reueq1f  3420  dfsbcq  3779  sbceqbid  3784  sbcbid  3835  sbcbi2  3839  eqsbc2  3846  sbcrext  3867  sbcabel  3872  ss2abdv  4060  psseq1  4087  psseq2  4088  ssconb  4137  uneq1  4156  difin2  4291  rcompleq  4295  reuun2  4314  sbcnel12g  4411  sbnfc2  4436  reldisj  4451  reldisjOLD  4452  undif4  4466  disjssun  4467  pssdifcom1  4489  pssdifcom2  4490  sbcssg  4523  eltpg  4689  raltpg  4702  rextpg  4703  r19.12sn  4724  intmin4  4981  dfiun2g  5033  dfiun2gOLD  5034  iindif1  5078  iindif2  5080  iinin2  5081  disjprgw  5143  disjprg  5144  disjxun  5146  breq  5150  breq1  5151  breq2  5152  treq  5273  reusv2lem5  5400  rexxfrd  5407  rexxfr2d  5409  rexxfrd2  5411  rabxfrd  5415  opthg2  5479  oteqex2  5499  oteqex  5500  poeq1  5591  soeq1  5609  freq1  5646  weeq1  5664  weeq2  5665  opthprc  5740  wesn  5764  releq  5776  sbcrel  5780  eqrel  5784  eqrelrel  5797  xpiindi  5835  dmopab2rex  5917  dfres3  5986  brres  5988  resieq  5992  dmsnopg  6212  dfco2a  6245  dfpo2  6295  ordeq  6371  limeq  6376  ordunisssuc  6470  iotaeq  6508  sniota  6534  sbcfung  6572  imadif  6632  fneq1  6640  fneq2  6641  feq1  6698  feq2  6699  feq3  6700  sbcfng  6714  sbcfg  6715  f1eq1  6782  f1eq2  6783  f1eq3  6784  foeq1  6801  foeq2  6802  foeq3  6803  f1oeq1  6821  f1oeq2  6822  f1oeq3  6823  mpteqb  7017  rexrnmptw  7096  rexrnmpt  7098  dffo3  7103  dffo3f  7107  fmptco  7129  dff13  7257  f1imaeq  7267  f1imapss  7268  cbvexfo  7291  f1eqcocnv  7302  f1eqcocnvOLD  7303  fliftcnv  7311  isoeq1  7317  isoeq2  7318  isoeq3  7319  isoeq4  7320  isoeq5  7321  isomin  7337  isowe  7349  eqfunresadj  7360  imaeqsalv  7364  nfriotadw  7376  mpoeq123  7484  rexrnmpo  7551  iunpw  7762  tfinds  7853  fiun  7933  f1iun  7934  opiota  8049  xpord3pred  8143  ottpos  8227  dmtpos  8229  onoviun  8349  smoeq  8356  smoiso2  8375  tfr2b  8402  oarec  8568  oeeui  8608  nnacan  8634  nnmcan  8640  ereq1  8716  ereq2  8717  elecg  8752  ereldm  8757  ixpiin  8924  boxriin  8940  boxcutc  8941  omxpenlem  9079  enfiALT  9197  nnsdomo  9240  isfinite2  9307  ixpfi2  9356  elfi2  9415  fipwss  9430  ttrclse  9728  ennum  9948  cardsdom2  9989  aleph11  10085  alephiso  10099  fin23lem26  10326  compssiso  10375  isf34lem4  10378  isfin5-2  10392  fin1a2lem5  10405  brdom7disj  10532  brdom6disj  10533  fpwwe2lem7  10638  fpwwe2lem11  10642  fpwwe2lem12  10643  genpass  11010  ltasr  11101  axpre-lttri  11166  infm3  12180  creur  12213  eqreznegel  12925  rpneg  13013  ltxr  13102  icoshftf1o  13458  elfzm11  13579  elfzomelpfzo  13743  nn0ennn  13951  nnesq  14197  hashbclem  14418  hashf1lem1  14422  hashf1lem1OLD  14423  leiso  14427  fz1isolem  14429  pr2pwpr  14447  repsdf2  14735  dfrtrclrec2  15012  rexfiuz  15301  cau4  15310  ello1mpt2  15473  o1lo1  15488  fsumcom2  15727  incexc2  15791  fprodcom2  15935  dvdsflip  16267  bitsmod  16384  bitscmp  16386  smueqlem  16438  divgcdcoprm0  16609  hashdvds  16715  prmreclem2  16857  vdwapun  16914  vdwmc2  16919  imasaddfnlem  17481  comfeq  17657  oppcsect  17732  funcres2b  17854  funcpropd  17860  fullpropd  17880  fthpropd  17881  fthres2b  17890  fthres2c  17891  fullres2c  17899  ffthres2c  17900  fucsect  17935  fucinv  17936  setcsect  18049  pospropd  18290  tosso  18382  odulatb  18397  oduclatb  18470  odudlatb  18488  isipodrs  18500  mgmhmpropd  18629  issgrpv  18652  issgrpn0  18653  mndpropd  18690  mhmpropd  18720  issubm2  18727  efmnd1bas  18816  grppropd  18879  grpinvcnv  18934  conjghm  19170  conjnmzb  19174  ghmpropd  19177  gapm  19218  symg1bas  19306  pmtrfrn  19374  cmnpropd  19707  ablpropd  19708  eqgabl  19750  gsumcom2  19891  dmdprd  19916  dprdw  19928  subgdmdprd  19952  pgpfac1lem2  19993  pgpfac1lem4  19996  rngpropd  20075  ringpropd  20183  crngpropd  20184  crngunit  20276  unitpropd  20315  isnirred  20318  issubrng  20443  subrngpropd  20464  resrhm2b  20500  subrgpropd  20506  rhmpropd  20507  rngcsect  20528  ringcsect  20562  drngpropd  20620  fldpropd  20621  acsfn1p  20646  abvpropd  20681  lmodprop2d  20766  lsspropd  20861  lmhmpropd  20917  lbspropd  20943  lmhmlvec  20954  lvecprop2d  21013  lvecpropd  21014  df2idl2rng  21109  opprdomn  21209  fiidomfld  21217  pzriprnglem10  21351  phlpropd  21519  assapropd  21737  psrbagconf1o  21800  psrbagconf1oOLD  21801  mplmonmul  21903  ismhp3  21996  mat1dimbas  22295  tpspropd  22761  tgss2  22811  lmbr2  23084  ist1-2  23172  ist1-3  23174  subislly  23306  dissnlocfin  23354  iskgen3  23374  txcnmpt  23449  hausdiag  23470  hauseqlcld  23471  xkococnlem  23484  tgqtop  23537  txhmeo  23628  uffix2  23749  ufildr  23756  txflf  23831  tgphaus  23942  qustgplem  23946  qustgphaus  23948  xpsdsval  24208  blin  24248  blres  24258  xmeterval  24259  xmspropd  24300  mspropd  24301  setsms  24309  metequiv  24339  metustsym  24385  restmetu  24400  ngppropd  24467  xrtgioo  24643  metdsge  24686  icopnfcnv  24788  iccpnfcnv  24790  lmhmclm  24935  lmmbr  25107  equivcmet  25166  cmspropd  25198  iunmbl2  25407  ioombl1lem4  25411  mbfaddlem  25510  i1fmullem  25544  itg1mulc  25555  iblcnlem1  25638  iblrelem  25641  iblre  25644  iblcn  25649  limcun  25745  mvth  25846  ofmulrt  26135  resinf1o  26386  quad2  26686  1cubr  26689  dcubic  26693  wilthlem2  26916  dvdsflf1o  27034  dvdsflsumcom  27035  fsumvma  27061  vmasum  27064  logfac2  27065  logfaclbnd  27070  dchrelbas3  27086  lgsquadlem1  27228  lgsquadlem2  27229  eqscut2  27654  mulsrid  27928  readdscl  28109  ax5seg  28631  ushgredgedg  28921  ushgredgedgloop  28923  nbumgrvtx  29038  upgriswlk  29333  wspniunwspnon  29612  rusgrnumwwlkb0  29660  isclwwlknx  29724  clwwlknscsh  29750  clwwlknonel  29783  0trl  29810  0spth  29814  0clwlk  29818  0crct  29821  0cycl  29822  eupth2lem2  29907  eucrct2eupth  29933  fusgr2wsp2nb  30022  ocin  30984  chpsscon3  31191  chscllem2  31326  adjval  31578  pjimai  31864  mdsldmd1i  32019  elat2  32028  mdsymi  32099  sbceqbidf  32162  rmoxfrd  32168  rmounid  32170  disjxun0  32240  disjrdx  32257  eqrelrd2  32280  fmptcof2  32317  ofpreima  32325  funcnv5mpt  32328  ressupprn  32347  1stpreima  32363  2ndpreima  32364  fpwrelmapffslem  32392  qsxpid  32916  grplsm0l  32955  opprlidlabs  33041  ressply1mon1p  33099  algextdeglem6  33235  smatrcl  33242  locfinreflem  33286  zarcls  33320  zhmnrg  33413  qqhval2  33428  ismntop  33472  reprsuc  34093  reprdifc  34105  bnj919  34244  bnj956  34253  bnj976  34254  bnj1366  34306  bnj916  34410  satfvsucsuc  34822  satfdm  34826  dmopab3rexdif  34862  sscoid  35357  dfrdg4  35395  altopthbg  35412  broutsideof3  35570  bj-nnfbi  36070  bj-cbvexdv  36145  bj-sbievw  36193  mobidvALT  36203  bj-restuni  36445  bj-elid6  36518  cbveud  36720  cbvreud  36721  exrecfnlem  36727  wl-ifp-ncond2  36813  wl-ifpimpr  36814  wl-3xorbi123d  36823  wl-sb8eut  36909  wl-sb8mot  36910  wl-clabtv  36926  wl-clabt  36927  poimirlem17  36972  poimirlem19  36974  poimirlem20  36975  poimirlem25  36980  ftc1anclem5  37032  istotbnd3  37106  sstotbnd  37110  heibor  37156  isass  37181  isidlc  37350  smprngopr  37387  brvvdif  37598  elecALTV  37601  eqrel2  37635  dmecd  37640  relcnveq2  37659  elrelscnveq2  37830  extssr  37846  elrefrelsrel  37857  refreleq  37858  elcnvrefrelsrel  37873  elsymrelsrel  37894  symreleq  37895  eltrrelsrel  37918  trreleq  37919  eleqvrelsrel  37931  eqvreleq  37939  redundpim3  37967  erALTVeq1  38006  elfunsALTVfunALTV  38034  eldisjsdisj  38064  eldisjeq  38078  disjsuc  38096  parteq1  38111  parteq2  38112  islshpsm  38317  lcvexchlem1  38371  opcon1b  38535  isat3  38644  glbconN  38714  glbconNOLD  38715  cdleme32fva  39775  cdlemg2cex  39929  dibelval3  40485  dib1dim  40503  doch11  40711  dochsordN  40712  mapdordlem1a  40972  mapd11  40977  mapdsord  40993  mapdcnv11N  40997  mapd0  41003  sn-iotalem  41508  ricfld  41572  fsuppind  41628  mrefg2  41911  jm2.23  42201  wepwsolem  42250  dnwech  42256  islssfg2  42279  gicabl  42307  isdomn3  42412  onsupmaxb  42454  onsupeqnmax  42462  orddif0suc  42484  oadif1lem  42595  oadif1  42596  fzunt  42672  fzuntd  42673  fzunt1d  42674  fzuntgd  42675  ifpbi2  42684  ifpbi3  42685  ifpbi1  42694  ifpbi12  42705  ifpbi13  42706  ontric3g  42739  pwinfig  42778  inintabd  42796  cnvcnvintabd  42817  cnvintabd  42820  intimag  42873  briunov2  42899  heeq12  42993  sbcheg  42996  uneqsn  43242  ntrneineine0lem  43300  ntrneineine1lem  43301  ntrneik2  43309  ntrneix2  43310  ntrneik13  43315  ntrneix13  43316  ralbidar  43670  rexbidar  43671  trsbc  43767  iindif2f  44319  rnmptpr  44338  iccintsng  44698  xlimres  44999  fsetsniunop  46221  fsetsnprcnex  46227  fcoresf1ob  46245  f1cof1b  46247  f1ocof1ob  46251  dfateq12d  46296  aov0nbovbi  46365  fnotaovb  46368  ichbidv  46583  sprsymrelf  46625  prprsprreu  46649  prprreueq  46650  rngcsectALTV  47115  ringcsectALTV  47149  lindslinindsimp2lem5  47308  opndisj  47700  i0oii  47717  io1ii  47718  iscnrm3lem2  47732