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  578  orbi2d  915  orbi1d  916  ifpbi123d  1078  3orbi123d  1437  3anbi123d  1438  nanbi1  1501  nanbi2  1502  xorbi12d  1525  hadbi123d  1595  had0  1604  cadbi123d  1610  nfbiit  1851  nfbidv  1922  sbequ  2083  nfbidf  2224  drex1v  2373  drnf1v  2374  drnf1vOLD  2375  drex1  2445  drnf1  2447  sb4b  2479  drsb1  2499  eujustALT  2571  eubi  2583  eleq1ab  2715  eqeq1d  2737  eqeq1dALT  2738  eqeq2d  2746  abbi  2800  eleq1w  2817  eleq2w  2818  eleq1d  2819  eleq2d  2820  eleq2dALT  2821  eqabdv  2868  nfceqdf  2894  drnfc1  2918  drnfc2  2919  neleq12d  3041  ralbidv2  3159  rexbidv2  3160  r19.21t  3236  r19.23t  3238  rexbida  3254  rexeq  3301  raleqbidvvOLD  3314  cbvraldva2  3327  cbvrexdva2OLD  3329  raleqf  3332  rexeqfOLD  3334  ralcom2  3356  rmobidva  3374  reubidva  3375  rmobida  3385  reubida  3386  rmoeq1  3395  reueq1  3396  rmoeq1OLD  3397  reueq1OLD  3398  reueqbidv  3402  rmoeq1f  3403  reueq1f  3404  dfsbcq  3767  sbceqbid  3772  sbcbid  3820  sbcbi2  3824  eqsbc2  3829  sbcrext  3848  sbcabel  3853  ralss  4033  rexss  4034  psseq1  4065  psseq2  4066  ssconb  4117  uneq1  4136  difin2  4276  rcompleq  4280  reuun2  4300  sbcnel12g  4389  sbnfc2  4414  reldisj  4428  undif4  4442  disjssun  4443  pssdifcom1  4465  pssdifcom2  4466  sbcssg  4495  eltpg  4662  raltpg  4674  rextpg  4675  r19.12sn  4696  intmin4  4953  dfiun2g  5006  dfiun2gOLD  5007  iindif1  5051  iindif2  5053  iinin2  5054  disjprg  5115  disjxun  5117  breq  5121  breq1  5122  breq2  5123  treq  5237  reusv2lem5  5372  rexxfrd  5379  rexxfr2d  5381  rexxfrd2  5383  rabxfrd  5387  opthg2  5454  oteqex2  5474  oteqex  5475  poeq1  5564  soeq1  5582  freq1  5621  weeq1  5641  weeq2  5642  opthprc  5718  wesn  5743  releq  5755  sbcrel  5759  eqrel  5763  eqrelrel  5776  xpiindi  5815  dmopab2rex  5897  dfres3  5971  brres  5973  resieq  5977  dmsnopg  6202  dfco2a  6235  dfpo2  6285  ordeq  6359  limeq  6364  ordunisssuc  6459  iotaeq  6495  sniota  6521  sbcfung  6559  imadif  6619  fneq1  6628  fneq2  6629  feq1  6685  feq2  6686  feq3  6687  sbcfng  6702  sbcfg  6703  f1eq1  6768  f1eq2  6769  f1eq3  6770  foeq1  6785  foeq2  6786  foeq3  6787  f1oeq1  6805  f1oeq2  6806  f1oeq3  6807  mpteqb  7004  rexrnmptw  7084  rexrnmpt  7086  dffo3  7091  dffo3f  7095  fmptco  7118  rexima  7229  dff13  7246  f1imaeq  7257  f1imapss  7258  cbvexfo  7282  f1eqcocnv  7293  fliftcnv  7303  isoeq1  7309  isoeq2  7310  isoeq3  7311  isoeq4  7312  isoeq5  7313  isomin  7329  isowe  7341  eqfunresadj  7352  imaeqsalvOLD  7356  nfriotadw  7368  mpoeq123  7477  rexrnmpo  7545  iunpw  7763  tfinds  7853  resf1extb  7928  fiun  7939  f1iun  7940  opiota  8056  xpord3pred  8149  ottpos  8233  dmtpos  8235  onoviun  8355  smoeq  8362  smoiso2  8381  tfr2b  8408  oarec  8572  oeeui  8612  nnacan  8638  nnmcan  8644  ereq1  8724  ereq2  8725  elecg  8761  ereldm  8767  ixpiin  8936  boxriin  8952  boxcutc  8953  omxpenlem  9085  enfiALT  9200  nnsdomo  9240  isfinite2  9304  ixpfi2  9360  elfi2  9424  fipwss  9439  ttrclse  9739  ennum  9959  cardsdom2  10000  aleph11  10096  alephiso  10110  fin23lem26  10337  compssiso  10386  isf34lem4  10389  isfin5-2  10403  fin1a2lem5  10416  brdom7disj  10543  brdom6disj  10544  fpwwe2lem7  10649  fpwwe2lem11  10653  fpwwe2lem12  10654  genpass  11021  ltasr  11112  axpre-lttri  11177  infm3  12199  creur  12232  eqreznegel  12948  rpneg  13039  ltxr  13129  icoshftf1o  13489  elfzm11  13610  elfzomelpfzo  13785  nn0ennn  13995  nnesq  14243  hashbclem  14468  hashf1lem1  14471  leiso  14475  fz1isolem  14477  pr2pwpr  14495  repsdf2  14794  dfrtrclrec2  15075  rexfiuz  15364  cau4  15373  ello1mpt2  15536  o1lo1  15551  fsumcom2  15788  incexc2  15852  fprodcom2  15998  dvdsflip  16334  bitsmod  16453  bitscmp  16455  smueqlem  16507  divgcdcoprm0  16682  hashdvds  16792  prmreclem2  16935  vdwapun  16992  vdwmc2  16997  imasaddfnlem  17540  comfeq  17716  oppcsect  17789  funcres2b  17908  funcpropd  17913  fullpropd  17933  fthpropd  17934  fthres2b  17943  fthres2c  17944  fullres2c  17952  ffthres2c  17953  fucsect  17986  fucinv  17987  setcsect  18100  pospropd  18335  tosso  18427  odulatb  18442  oduclatb  18515  odudlatb  18533  isipodrs  18545  mgmhmpropd  18674  issgrpv  18697  issgrpn0  18698  mndpropd  18735  mhmpropd  18768  issubm2  18780  efmnd1bas  18869  grppropd  18932  grpinvcnv  18987  conjghm  19230  conjnmzb  19234  ghmpropd  19237  gapm  19287  symg1bas  19370  pmtrfrn  19437  cmnpropd  19770  ablpropd  19771  eqgabl  19813  gsumcom2  19954  dmdprd  19979  dprdw  19991  subgdmdprd  20015  pgpfac1lem2  20056  pgpfac1lem4  20059  rngpropd  20132  ringpropd  20246  crngpropd  20247  crngunit  20336  unitpropd  20375  isnirred  20378  nzrpropd  20478  issubrng  20505  subrngpropd  20526  resrhm2b  20560  subrgpropd  20566  rhmpropd  20567  rngcsect  20594  ringcsect  20628  isdomn3  20673  drngpropd  20727  fldpropd  20728  fiidomfld  20732  acsfn1p  20757  abvpropd  20793  lmodprop2d  20879  lsspropd  20973  lmhmpropd  21029  lbspropd  21055  lmhmlvec  21066  lvecprop2d  21125  lvecpropd  21126  df2idl2rng  21215  pzriprnglem10  21449  phlpropd  21613  assapropd  21830  psrbagconf1o  21887  mplmonmul  21992  ismhp3  22078  mat1dimbas  22408  tpspropd  22874  tgss2  22923  lmbr2  23195  ist1-2  23283  ist1-3  23285  subislly  23417  dissnlocfin  23465  iskgen3  23485  txcnmpt  23560  hausdiag  23581  hauseqlcld  23582  xkococnlem  23595  tgqtop  23648  txhmeo  23739  uffix2  23860  ufildr  23867  txflf  23942  tgphaus  24053  qustgplem  24057  qustgphaus  24059  xpsdsval  24318  blin  24358  blres  24368  xmeterval  24369  xmspropd  24410  mspropd  24411  setsms  24417  metequiv  24446  metustsym  24492  restmetu  24507  ngppropd  24574  xrtgioo  24744  metdsge  24787  icopnfcnv  24889  iccpnfcnv  24891  lmhmclm  25036  lmmbr  25208  equivcmet  25267  cmspropd  25299  iunmbl2  25508  ioombl1lem4  25512  mbfaddlem  25611  i1fmullem  25645  itg1mulc  25655  iblcnlem1  25739  iblrelem  25742  iblre  25745  iblcn  25750  limcun  25846  mvth  25947  ofmulrt  26239  resinf1o  26495  quad2  26799  1cubr  26802  dcubic  26806  wilthlem2  27029  dvdsflf1o  27147  dvdsflsumcom  27148  fsumvma  27174  vmasum  27177  logfac2  27178  logfaclbnd  27183  dchrelbas3  27199  lgsquadlem1  27341  lgsquadlem2  27342  eqscut2  27768  mulsrid  28056  readdscl  28348  ax5seg  28863  ushgredgedg  29154  ushgredgedgloop  29156  nbumgrvtx  29271  upgriswlk  29567  wspniunwspnon  29851  rusgrnumwwlkb0  29899  isclwwlknx  29963  clwwlknscsh  29989  clwwlknonel  30022  0trl  30049  0spth  30053  0clwlk  30057  0crct  30060  0cycl  30061  eupth2lem2  30146  eucrct2eupth  30172  fusgr2wsp2nb  30261  ocin  31223  chpsscon3  31430  chscllem2  31565  adjval  31817  pjimai  32103  mdsldmd1i  32258  elat2  32267  mdsymi  32338  sbceqbidf  32414  rmoxfrd  32420  rmounid  32422  disjxun0  32501  disjrdx  32518  eqrelrd2  32542  fmptcof2  32581  ofpreima  32589  funcnv5mpt  32592  ressupprn  32613  1stpreima  32630  2ndpreima  32631  fpwrelmapffslem  32655  domnpropd  33217  idompropd  33218  subsdrg  33238  qsxpid  33323  grplsm0l  33364  opprlidlabs  33446  ressply1mon1p  33527  algextdeglem6  33702  smatrcl  33773  locfinreflem  33817  zarcls  33851  zhmnrg  33942  qqhval2  33959  ismntop  34003  reprsuc  34593  reprdifc  34605  bnj919  34744  bnj956  34753  bnj976  34754  bnj1366  34806  bnj916  34910  satfvsucsuc  35333  satfdm  35337  dmopab3rexdif  35373  rexxfr3dALT  35607  sscoid  35877  dfrdg4  35915  altopthbg  35932  broutsideof3  36090  rmoeqbidv  36177  sbequbidv  36178  disjeq12dv  36179  ixpeq12dv  36180  cbvmodavw  36214  cbveudavw  36215  cbvrmodavw  36216  cbvreudavw  36217  cbvsbdavw  36218  cbvsbdavw2  36219  cbvabdavw  36220  cbvsbcdavw  36221  cbvsbcdavw2  36222  cbvdisjdavw  36232  cbvrmodavw2  36247  cbvreudavw2  36248  cbvdisjdavw2  36253  bj-nnfbi  36689  bj-cbvexdv  36764  bj-sbievw  36811  mobidvALT  36821  bj-restuni  37061  bj-elid6  37134  cbveud  37336  cbvreud  37337  exrecfnlem  37343  wl-ifp-ncond2  37429  wl-ifpimpr  37430  wl-3xorbi123d  37439  wl-sb8eut  37542  wl-sb8eutv  37543  wl-sb8mot  37544  wl-sb8motv  37545  wl-clabtv  37561  wl-clabt  37562  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem25  37615  ftc1anclem5  37667  istotbnd3  37741  sstotbnd  37745  heibor  37791  isass  37816  isidlc  37985  smprngopr  38022  brvvdif  38227  elecALTV  38230  eqrel2  38263  dmecd  38268  relcnveq2  38287  elrelscnveq2  38457  extssr  38473  elrefrelsrel  38484  refreleq  38485  elcnvrefrelsrel  38500  elsymrelsrel  38521  symreleq  38522  eltrrelsrel  38545  trreleq  38546  eleqvrelsrel  38558  eqvreleq  38566  redundpim3  38594  erALTVeq1  38633  elfunsALTVfunALTV  38661  eldisjsdisj  38691  eldisjeq  38705  disjsuc  38723  parteq1  38738  parteq2  38739  islshpsm  38944  lcvexchlem1  38998  opcon1b  39162  isat3  39271  glbconN  39341  glbconNOLD  39342  cdleme32fva  40402  cdlemg2cex  40556  dibelval3  41112  dib1dim  41130  doch11  41338  dochsordN  41339  mapdordlem1a  41599  mapd11  41604  mapdsord  41620  mapdcnv11N  41624  mapd0  41630  sn-iotalem  42218  ricfld  42500  fimgmcyc  42504  fsuppind  42560  mrefg2  42677  jm2.23  42967  wepwsolem  43013  dnwech  43019  islssfg2  43042  gicabl  43070  onsupmaxb  43210  onsupeqnmax  43218  orddif0suc  43239  oadif1lem  43350  oadif1  43351  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  ifpbi2  43438  ifpbi3  43439  ifpbi1  43448  ifpbi12  43459  ifpbi13  43460  ontric3g  43493  pwinfig  43532  inintabd  43550  cnvcnvintabd  43571  cnvintabd  43574  intimag  43627  briunov2  43653  heeq12  43747  sbcheg  43750  uneqsn  43996  ntrneineine0lem  44054  ntrneineine1lem  44055  ntrneik2  44063  ntrneix2  44064  ntrneik13  44069  ntrneix13  44070  ralbidar  44417  rexbidar  44418  trsbc  44513  relpeq1  44917  relpeq2  44918  relpeq3  44919  relpeq4  44920  relpeq5  44921  n0abso  44949  modelaxreplem3  44953  iindif2f  45132  rnmptpr  45149  iccintsng  45500  xlimres  45798  fsetsniunop  47026  fsetsnprcnex  47032  fcoresf1ob  47050  f1cof1b  47054  f1ocof1ob  47058  dfateq12d  47103  aov0nbovbi  47172  fnotaovb  47175  ichbidv  47415  sprsymrelf  47457  prprsprreu  47481  prprreueq  47482  edgusgrclnbfin  47803  dfclnbgr6  47817  dfnbgr6  47818  isubgredg  47827  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  rngcsectALTV  48198  ringcsectALTV  48232  lindslinindsimp2lem5  48386  opndisj  48825  i0oii  48842  io1ii  48843  iscnrm3lem2  48857  thincpropd  49276  termcpropd  49336