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 206

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 207

This theorem is referenced by:  bibi1d  343  pm5.32rd  577  orbi2d  914  orbi1d  915  ifpbi123d  1079  3orbi123d  1435  3anbi123d  1436  nanbi1  1498  nanbi2  1499  xorbi12d  1522  hadbi123d  1592  had0  1601  cadbi123d  1607  nfbiit  1849  nfbidv  1921  sbequ  2083  nfbidf  2225  drex1v  2377  drnf1v  2378  drnf1vOLD  2379  drex1  2449  drnf1  2451  sb4b  2483  drsb1  2503  eujustALT  2575  eubi  2587  eleq1ab  2719  eqeq1d  2742  eqeq1dALT  2743  eqeq2d  2751  abbi  2810  eleq1w  2827  eleq2w  2828  eleq1d  2829  eleq2d  2830  eleq2dALT  2831  eqabdv  2878  nfceqdf  2904  drnfc1  2928  drnfc1OLD  2929  drnfc2  2930  drnfc2OLD  2931  neleq12d  3057  ralrexbidOLD  3113  ralbidv2  3180  rexbidv2  3181  r19.21t  3259  r19.23t  3261  ralbidaOLD  3277  rexbida  3278  rexeq  3330  raleqbidvvOLD  3343  cbvraldva2  3356  cbvrexdva2OLD  3358  raleqf  3361  rexeqfOLD  3363  ralcom2  3385  rmobidva  3403  reubidva  3404  rmobida  3414  reubida  3415  rmoeq1  3425  reueq1  3426  rmoeq1OLD  3427  reueq1OLD  3428  rmoeq1f  3431  reueq1f  3432  dfsbcq  3806  sbceqbid  3811  sbcbid  3863  sbcbi2  3867  eqsbc2  3873  sbcrext  3895  sbcabel  3900  psseq1  4113  psseq2  4114  ssconb  4165  uneq1  4184  difin2  4320  rcompleq  4324  reuun2  4344  sbcnel12g  4437  sbnfc2  4462  reldisj  4476  undif4  4490  disjssun  4491  pssdifcom1  4513  pssdifcom2  4514  sbcssg  4543  eltpg  4709  raltpg  4723  rextpg  4724  r19.12sn  4745  intmin4  5001  dfiun2g  5053  dfiun2gOLD  5054  iindif1  5098  iindif2  5100  iinin2  5101  disjprg  5162  disjxun  5164  breq  5168  breq1  5169  breq2  5170  treq  5291  reusv2lem5  5420  rexxfrd  5427  rexxfr2d  5429  rexxfrd2  5431  rabxfrd  5435  opthg2  5499  oteqex2  5518  oteqex  5519  poeq1  5610  soeq1  5629  freq1  5667  weeq1  5687  weeq2  5688  opthprc  5764  wesn  5788  releq  5800  sbcrel  5804  eqrel  5808  eqrelrel  5821  xpiindi  5860  dmopab2rex  5942  dfres3  6014  brres  6016  resieq  6020  dmsnopg  6244  dfco2a  6277  dfpo2  6327  ordeq  6402  limeq  6407  ordunisssuc  6501  iotaeq  6538  sniota  6564  sbcfung  6602  imadif  6662  fneq1  6670  fneq2  6671  feq1  6728  feq2  6729  feq3  6730  sbcfng  6744  sbcfg  6745  f1eq1  6812  f1eq2  6813  f1eq3  6814  foeq1  6830  foeq2  6831  foeq3  6832  f1oeq1  6850  f1oeq2  6851  f1oeq3  6852  mpteqb  7048  rexrnmptw  7129  rexrnmpt  7131  dffo3  7136  dffo3f  7140  fmptco  7163  rexima  7275  dff13  7292  f1imaeq  7302  f1imapss  7303  cbvexfo  7326  f1eqcocnv  7337  fliftcnv  7347  isoeq1  7353  isoeq2  7354  isoeq3  7355  isoeq4  7356  isoeq5  7357  isomin  7373  isowe  7385  eqfunresadj  7396  imaeqsalvOLD  7400  nfriotadw  7412  mpoeq123  7522  rexrnmpo  7590  iunpw  7806  tfinds  7897  fiun  7983  f1iun  7984  opiota  8100  xpord3pred  8193  ottpos  8277  dmtpos  8279  onoviun  8399  smoeq  8406  smoiso2  8425  tfr2b  8452  oarec  8618  oeeui  8658  nnacan  8684  nnmcan  8690  ereq1  8770  ereq2  8771  elecg  8807  ereldm  8813  ixpiin  8982  boxriin  8998  boxcutc  8999  omxpenlem  9139  enfiALT  9254  nnsdomo  9297  isfinite2  9362  ixpfi2  9420  elfi2  9483  fipwss  9498  ttrclse  9796  ennum  10016  cardsdom2  10057  aleph11  10153  alephiso  10167  fin23lem26  10394  compssiso  10443  isf34lem4  10446  isfin5-2  10460  fin1a2lem5  10473  brdom7disj  10600  brdom6disj  10601  fpwwe2lem7  10706  fpwwe2lem11  10710  fpwwe2lem12  10711  genpass  11078  ltasr  11169  axpre-lttri  11234  infm3  12254  creur  12287  eqreznegel  12999  rpneg  13089  ltxr  13178  icoshftf1o  13534  elfzm11  13655  elfzomelpfzo  13821  nn0ennn  14030  nnesq  14276  hashbclem  14501  hashf1lem1  14504  leiso  14508  fz1isolem  14510  pr2pwpr  14528  repsdf2  14826  dfrtrclrec2  15107  rexfiuz  15396  cau4  15405  ello1mpt2  15568  o1lo1  15583  fsumcom2  15822  incexc2  15886  fprodcom2  16032  dvdsflip  16365  bitsmod  16482  bitscmp  16484  smueqlem  16536  divgcdcoprm0  16712  hashdvds  16822  prmreclem2  16964  vdwapun  17021  vdwmc2  17026  imasaddfnlem  17588  comfeq  17764  oppcsect  17839  funcres2b  17961  funcpropd  17967  fullpropd  17987  fthpropd  17988  fthres2b  17997  fthres2c  17998  fullres2c  18006  ffthres2c  18007  fucsect  18042  fucinv  18043  setcsect  18156  pospropd  18397  tosso  18489  odulatb  18504  oduclatb  18577  odudlatb  18595  isipodrs  18607  mgmhmpropd  18736  issgrpv  18759  issgrpn0  18760  mndpropd  18797  mhmpropd  18827  issubm2  18839  efmnd1bas  18928  grppropd  18991  grpinvcnv  19046  conjghm  19289  conjnmzb  19293  ghmpropd  19296  gapm  19346  symg1bas  19432  pmtrfrn  19500  cmnpropd  19833  ablpropd  19834  eqgabl  19876  gsumcom2  20017  dmdprd  20042  dprdw  20054  subgdmdprd  20078  pgpfac1lem2  20119  pgpfac1lem4  20122  rngpropd  20201  ringpropd  20311  crngpropd  20312  crngunit  20404  unitpropd  20443  isnirred  20446  nzrpropd  20546  issubrng  20573  subrngpropd  20594  resrhm2b  20630  subrgpropd  20636  rhmpropd  20637  rngcsect  20658  ringcsect  20692  isdomn3  20737  drngpropd  20791  fldpropd  20792  fiidomfld  20797  acsfn1p  20822  abvpropd  20858  lmodprop2d  20944  lsspropd  21039  lmhmpropd  21095  lbspropd  21121  lmhmlvec  21132  lvecprop2d  21191  lvecpropd  21192  df2idl2rng  21289  pzriprnglem10  21524  phlpropd  21696  assapropd  21915  psrbagconf1o  21972  mplmonmul  22077  ismhp3  22169  mat1dimbas  22499  tpspropd  22965  tgss2  23015  lmbr2  23288  ist1-2  23376  ist1-3  23378  subislly  23510  dissnlocfin  23558  iskgen3  23578  txcnmpt  23653  hausdiag  23674  hauseqlcld  23675  xkococnlem  23688  tgqtop  23741  txhmeo  23832  uffix2  23953  ufildr  23960  txflf  24035  tgphaus  24146  qustgplem  24150  qustgphaus  24152  xpsdsval  24412  blin  24452  blres  24462  xmeterval  24463  xmspropd  24504  mspropd  24505  setsms  24513  metequiv  24543  metustsym  24589  restmetu  24604  ngppropd  24671  xrtgioo  24847  metdsge  24890  icopnfcnv  24992  iccpnfcnv  24994  lmhmclm  25139  lmmbr  25311  equivcmet  25370  cmspropd  25402  iunmbl2  25611  ioombl1lem4  25615  mbfaddlem  25714  i1fmullem  25748  itg1mulc  25759  iblcnlem1  25843  iblrelem  25846  iblre  25849  iblcn  25854  limcun  25950  mvth  26051  ofmulrt  26341  resinf1o  26596  quad2  26900  1cubr  26903  dcubic  26907  wilthlem2  27130  dvdsflf1o  27248  dvdsflsumcom  27249  fsumvma  27275  vmasum  27278  logfac2  27279  logfaclbnd  27284  dchrelbas3  27300  lgsquadlem1  27442  lgsquadlem2  27443  eqscut2  27869  mulsrid  28157  readdscl  28449  ax5seg  28971  ushgredgedg  29264  ushgredgedgloop  29266  nbumgrvtx  29381  upgriswlk  29677  wspniunwspnon  29956  rusgrnumwwlkb0  30004  isclwwlknx  30068  clwwlknscsh  30094  clwwlknonel  30127  0trl  30154  0spth  30158  0clwlk  30162  0crct  30165  0cycl  30166  eupth2lem2  30251  eucrct2eupth  30277  fusgr2wsp2nb  30366  ocin  31328  chpsscon3  31535  chscllem2  31670  adjval  31922  pjimai  32208  mdsldmd1i  32363  elat2  32372  mdsymi  32443  sbceqbidf  32515  rmoxfrd  32521  rmounid  32523  disjxun0  32596  disjrdx  32613  eqrelrd2  32638  fmptcof2  32675  ofpreima  32683  funcnv5mpt  32686  ressupprn  32702  1stpreima  32718  2ndpreima  32719  fpwrelmapffslem  32746  qsxpid  33355  grplsm0l  33396  opprlidlabs  33478  ressply1mon1p  33558  algextdeglem6  33713  smatrcl  33742  locfinreflem  33786  zarcls  33820  zhmnrg  33913  qqhval2  33928  ismntop  33972  reprsuc  34592  reprdifc  34604  bnj919  34743  bnj956  34752  bnj976  34753  bnj1366  34805  bnj916  34909  satfvsucsuc  35333  satfdm  35337  dmopab3rexdif  35373  rexxfr3dALT  35607  sscoid  35877  dfrdg4  35915  altopthbg  35932  broutsideof3  36090  rmoeqbidv  36177  reueqbidv  36179  sbequbidv  36180  disjeq12dv  36181  ixpeq12dv  36182  cbvmodavw  36216  cbveudavw  36217  cbvrmodavw  36218  cbvreudavw  36219  cbvsbdavw  36220  cbvsbdavw2  36221  cbvabdavw  36222  cbvsbcdavw  36223  cbvsbcdavw2  36224  cbvdisjdavw  36234  cbvrmodavw2  36249  cbvreudavw2  36250  cbvdisjdavw2  36255  bj-nnfbi  36691  bj-cbvexdv  36766  bj-sbievw  36813  mobidvALT  36823  bj-restuni  37063  bj-elid6  37136  cbveud  37338  cbvreud  37339  exrecfnlem  37345  wl-ifp-ncond2  37431  wl-ifpimpr  37432  wl-3xorbi123d  37441  wl-sb8eut  37532  wl-sb8eutv  37533  wl-sb8mot  37534  wl-sb8motv  37535  wl-clabtv  37551  wl-clabt  37552  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem25  37605  ftc1anclem5  37657  istotbnd3  37731  sstotbnd  37735  heibor  37781  isass  37806  isidlc  37975  smprngopr  38012  brvvdif  38219  elecALTV  38222  eqrel2  38255  dmecd  38260  relcnveq2  38279  elrelscnveq2  38449  extssr  38465  elrefrelsrel  38476  refreleq  38477  elcnvrefrelsrel  38492  elsymrelsrel  38513  symreleq  38514  eltrrelsrel  38537  trreleq  38538  eleqvrelsrel  38550  eqvreleq  38558  redundpim3  38586  erALTVeq1  38625  elfunsALTVfunALTV  38653  eldisjsdisj  38683  eldisjeq  38697  disjsuc  38715  parteq1  38730  parteq2  38731  islshpsm  38936  lcvexchlem1  38990  opcon1b  39154  isat3  39263  glbconN  39333  glbconNOLD  39334  cdleme32fva  40394  cdlemg2cex  40548  dibelval3  41104  dib1dim  41122  doch11  41330  dochsordN  41331  mapdordlem1a  41591  mapd11  41596  mapdsord  41612  mapdcnv11N  41616  mapd0  41622  sn-iotalem  42214  ricfld  42485  fimgmcyc  42489  fsuppind  42545  mrefg2  42663  jm2.23  42953  wepwsolem  42999  dnwech  43005  islssfg2  43028  gicabl  43056  onsupmaxb  43200  onsupeqnmax  43208  orddif0suc  43230  oadif1lem  43341  oadif1  43342  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  ifpbi2  43429  ifpbi3  43430  ifpbi1  43439  ifpbi12  43450  ifpbi13  43451  ontric3g  43484  pwinfig  43523  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  intimag  43618  briunov2  43644  heeq12  43738  sbcheg  43741  uneqsn  43987  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneik2  44054  ntrneix2  44055  ntrneik13  44060  ntrneix13  44061  ralbidar  44414  rexbidar  44415  trsbc  44511  iindif2f  45065  rnmptpr  45084  iccintsng  45441  xlimres  45742  fsetsniunop  46964  fsetsnprcnex  46970  fcoresf1ob  46988  f1cof1b  46992  f1ocof1ob  46996  dfateq12d  47041  aov0nbovbi  47110  fnotaovb  47113  ichbidv  47327  sprsymrelf  47369  prprsprreu  47393  prprreueq  47394  edgusgrclnbfin  47714  dfclnbgr6  47728  dfnbgr6  47729  rngcsectALTV  47998  ringcsectALTV  48032  lindslinindsimp2lem5  48191  opndisj  48582  i0oii  48599  io1ii  48600  iscnrm3lem2  48614