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	bitrid 286	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 292	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  pm5.32rd  589  orbi2d  929  orbi1d  930  ifpbi123d  1095  3orbi123d  1463  3anbi123d  1464  nanbi1  1531  nanbi2  1532  xorbi12d  1555  hadbi123d  1625  had0OLD  1636  cadbi123d  1643  nfbiit  1884  nfbidv  1955  sbequ  2120  nfbidf  2260  drex1v  2399  drnf1v  2400  drex1  2470  drnf1  2472  sb4b  2504  drsb1  2524  eujustALT  2597  eubi  2609  eleq1ab  2740  eqeq1d  2762  eqeq1dALT  2763  eqeq2d  2771  abbi  2825  eleq1w  2843  eleq2w  2844  eleq1d  2845  eleq2d  2846  eleq2dALT  2847  eqabdv  2893  nfceqdf  2918  drnfc1  2941  drnfc2  2942  neleq12d  3066  ralbidv2  3181  rexbidv2  3182  r19.21t  3256  r19.23t  3258  rexbida  3274  rexeq  3315  cbvraldva2  3336  raleqf  3341  ralcom2  3362  rmobidva  3378  reubidva  3379  rmobida  3388  reubida  3389  rmoeq1  3396  reueq1  3397  reueqbidv  3401  rmoeq1f  3402  reueq1f  3403  dfsbcq  3741  sbceqbid  3746  sbcbid  3793  sbcbi2  3797  eqsbc2  3802  sbcrext  3820  sbcabel  3825  ralss  4004  rexss  4005  psseq1  4038  psseq2  4039  ssconb  4089  uneq1  4108  difin2  4247  rcompleq  4251  reuun2  4271  sbcnel12g  4372  sbnfc2  4397  reldisj  4406  undif4  4420  disjssun  4421  pssdifcom1  4445  pssdifcom2  4446  sbcssg  4477  eltpg  4647  raltpg  4659  rextpg  4660  r19.12sn  4681  intmin4  4937  dfiun2g  4988  iindif1  5035  iindif2  5037  iinin2  5038  disjprg  5099  disjxun  5101  breq  5105  breq1  5106  breq2  5107  treq  5219  reusv2lem5  5367  rexxfrd  5374  rexxfr2d  5376  rexxfrd2  5378  rabxfrd  5382  opthg2  5455  oteqex2  5476  oteqex  5477  poeq1  5566  soeq1  5584  freq1  5622  weeq1  5642  weeq2  5643  opthprc  5719  wesn  5744  releq  5757  sbcrel  5761  eqrel  5764  eqrelrel  5777  xpiindi  5815  dmopab2rex  5901  dfres3  5977  brres  5979  resieq  5983  dmsnopg  6209  dfco2a  6242  dfpo2  6294  ordeq  6364  limeq  6369  ordunisssuc  6466  iotaeq  6501  sniota  6524  sbcfung  6557  sbcfungOLD  6558  imadif  6618  fneq1  6624  fneq2  6625  feq1  6681  feq2  6682  feq3  6683  sbcfng  6700  sbcfg  6701  f1eq1  6767  f1eq2  6768  f1eq3  6769  foeq1  6786  foeq2  6787  foeq3  6788  f1oeq1  6806  f1oeq2  6807  f1oeq3  6808  mpteqb  7007  rexrnmptw  7089  rexrnmpt  7091  dffo3  7096  dffo3f  7100  fmptco  7124  rexima  7238  dff13  7252  f1imaeq  7263  f1imapss  7264  cbvexfo  7292  f1eqcocnv  7303  fliftcnv  7313  isoeq1  7319  isoeq2  7320  isoeq3  7321  isoeq4  7322  isoeq5  7323  isomin  7339  isowe  7351  eqfunresadj  7364  nfriotadw  7379  mpoeq123  7486  rexrnmpo  7554  iunpw  7771  tfinds  7857  resf1extb  7932  fiun  7941  f1iun  7942  opiota  8057  xpord3pred  8151  ottpos  8235  dmtpos  8237  onoviun  8333  smoeq  8340  smoiso2  8359  tfr2b  8386  oarec  8552  oeeui  8593  nnacan  8619  nnmcan  8625  ereq1  8707  ereq2  8708  elecg  8744  ereldm  8753  ixpiin  8934  boxriin  8950  boxcutc  8951  omxpenlem  9079  enfiALT  9185  nnsdomo  9216  isfinite2  9271  ixpfi2  9320  elfi2  9387  fipwss  9402  ttrclse  9709  ennum  9955  cardsdom2  9996  aleph11  10090  alephiso  10104  fin23lem26  10330  compssiso  10379  isf34lem4  10382  isfin5-2  10396  fin1a2lem5  10409  brdom7disj  10537  brdom6disj  10538  fpwwe2lem7  10649  fpwwe2lem11  10653  fpwwe2lem12  10654  genpass  11021  ltasr  11112  axpre-lttri  11177  infm3  12201  creur  12239  eqreznegel  12986  rpneg  13079  ltxr  13169  icoshftf1o  13530  elfzm11  13653  elfzomelpfzo  13831  nn0ennn  14046  nnesq  14294  hashbclem  14520  hashf1lem1  14523  leiso  14527  fz1isolem  14529  pr2pwpr  14547  repsdf2  14852  dfrtrclrec2  15134  rexfiuz  15438  cau4  15447  ello1mpt2  15612  o1lo1  15627  fsumcom2  15863  incexc2  15930  fprodcom2  16074  dvdsflip  16410  bitsmod  16529  bitscmp  16531  smueqlem  16583  divgcdcoprm0  16758  hashdvds  16869  prmreclem2  17012  vdwapun  17069  vdwmc2  17074  imasaddfnlem  17617  comfeq  17797  oppcsect  17870  funcres2b  17989  funcpropd  17994  fullpropd  18014  fthpropd  18015  fthres2b  18024  fthres2c  18025  fullres2c  18033  ffthres2c  18034  fucsect  18067  fucinv  18068  setcsect  18181  pospropd  18416  tosso  18508  odulatb  18525  oduclatb  18598  odudlatb  18616  isipodrs  18628  mgmhmpropd  18803  issgrpv  18826  issgrpn0  18827  mndpropd  18867  mhmpropd  18903  issubm2  18915  efmnd1bas  19005  grppropd  19078  grpinvcnv  19133  qsxpid  19303  conjghm  19379  conjnmzb  19383  ghmpropd  19386  gapm  19436  symg1bas  19521  pmtrfrn  19588  cmnpropd  19921  ablpropd  19922  eqgabl  19964  gsumcom2  20105  dmdprd  20130  dprdw  20142  subgdmdprd  20166  pgpfac1lem2  20207  pgpfac1lem4  20210  rngpropd  20312  ringpropd  20433  crngpropd  20434  crngunit  20522  unitpropd  20561  isnirred  20564  nzrpropd  20684  issubrng  20712  subrngpropd  20733  resrhm2b  20767  subrgpropd  20773  rhmpropd  20774  rngcsect  20801  ringcsect  20835  isdomn3  20879  drngpropd  20939  fldpropd  20940  fiidomfld  20944  acsfn1p  20968  abvpropd  21004  lmodprop2d  21111  lsspropd  21204  lmhmpropd  21260  lbspropd  21286  lmhmlvec  21297  lvecprop2d  21356  lvecpropd  21357  df2idl2rng  21461  pzriprnglem10  21706  phlpropd  21871  assapropd  22089  psrbagconf1o  22147  mplmonmul  22255  ismhp3  22373  mat1dimbas  22697  tpspropd  23166  tgss2  23215  lmbr2  23487  ist1-2  23575  ist1-3  23577  subislly  23710  dissnlocfin  23758  iskgen3  23778  txcnmpt  23853  hausdiag  23874  hauseqlcld  23875  xkococnlem  23888  tgqtop  23941  txhmeo  24032  uffix2  24153  ufildr  24160  txflf  24235  tgphaus  24346  qustgplem  24350  qustgphaus  24352  xpsdsval  24610  blin  24650  blres  24660  xmeterval  24661  xmspropd  24702  mspropd  24703  setsms  24709  metequiv  24738  metustsym  24784  restmetu  24799  ngppropd  24866  xrtgioo  25036  metdsge  25079  icopnfcnv  25173  iccpnfcnv  25175  lmhmclm  25318  lmmbr  25489  equivcmet  25548  cmspropd  25580  iunmbl2  25788  ioombl1lem4  25792  mbfaddlem  25891  i1fmullem  25925  itg1mulc  25935  iblcnlem1  26018  iblrelem  26021  iblre  26024  iblcn  26029  limcun  26125  mvth  26222  ofmulrt  26512  resinf1o  26776  quad2  27079  1cubr  27082  dcubic  27086  wilthlem2  27308  dvdsflf1o  27426  dvdsflsumcom  27427  fsumvma  27452  vmasum  27455  logfac2  27456  logfaclbnd  27461  dchrelbas3  27477  lgsquadlem1  27619  lgsquadlem2  27620  eqcuts2  28054  mulsrid  28381  z12sge0  28751  readdscl  28767  elplng  29140  plngcplem  29145  ax5seg  29398  ushgredgedg  29692  ushgredgedgloop  29694  nbumgrvtx  29809  upgriswlk  30103  wspniunwspnon  30394  rusgrnumwwlkb0  30445  isclwwlknx  30509  clwwlknscsh  30535  clwwlknonel  30568  0trl  30595  0spth  30599  0clwlk  30603  0crct  30606  0cycl  30607  eupth2lem2  30702  eucrct2eupth  30728  fusgr2wsp2nb  30817  ocin  31780  chpsscon3  31987  chscllem2  32122  adjval  32374  pjimai  32660  mdsldmd1i  32815  elat2  32824  mdsymi  32895  sbceqbidf  32965  rmoxfrd  32971  rmounid  32973  disjxun0  33050  disjrdx  33067  eqrelrd2  33092  fmptcof2  33133  ofpreima  33141  funcnv5mpt  33143  ressupprn  33165  1stpreima  33182  2ndpreima  33183  fpwrelmapffslem  33206  cntrval2  33614  domnpropd  33723  idompropd  33724  subsdrg  33742  grplsm0l  33835  opprlidlabs  33890  ressply1mon1p  33981  psrmonmul  34063  algextdeglem6  34235  smatrcl  34309  locfinreflem  34353  zarcls  34387  zhmnrg  34478  qqhval2  34495  ismntop  34539  reprsuc  35126  reprdifc  35138  bnj919  35280  bnj956  35289  bnj976  35290  bnj1366  35341  bnj916  35445  satfvsucsuc  35947  satfdm  35951  dmopab3rexdif  35987  rexxfr3dALT  36221  sscoid  36493  dfrdg4  36533  altopthbg  36551  broutsideof3  36709  rmoeqbidv  36836  sbequbidv  36837  disjeq12dv  36838  ixpeq12dv  36839  cbvmodavw  36873  cbveudavw  36874  cbvrmodavw  36875  cbvreudavw  36876  cbvsbdavw  36877  cbvsbdavw2  36878  cbvabdavw  36879  cbvsbcdavw  36880  cbvsbcdavw2  36881  cbvdisjdavw  36891  cbvrmodavw2  36906  cbvreudavw2  36907  cbvdisjdavw2  36912  bj-nnfbi  37483  bj-cbvexdv  37546  bj-sbievw  37593  mobidvALT  37603  bj-axreprepsep  37823  bj-restuni  37850  bj-elid6  37925  cbveud  38129  cbvreud  38130  exrecfnlem  38136  wl-ifp-ncond2  38222  wl-ifpimpr  38223  wl-3xorbi123d  38232  wl-sb8eut  38344  wl-sb8eutv  38345  wl-sb8mot  38346  wl-sb8motv  38347  wl-clabtv  38352  wl-clabt  38353  wl-eujustlem1  38354  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem25  38397  ftc1anclem5  38449  istotbnd3  38524  sstotbnd  38528  heibor  38574  isass  38599  isidlc  38768  smprngopr  38805  brvvdif  39019  elecALTV  39022  eqrel2  39056  dmecd  39061  relcnveq2  39080  eldmxrncnvepres  39185  eldmxrncnvepres2  39186  extssr  39340  elrefrelsrel  39351  refreleq  39352  elcnvrefrelsrel  39367  elrelscnveq2  39380  elsymrelsrel  39392  symreleq  39393  eltrrelsrel  39416  trreleq  39417  eleqvrelsrel  39429  eqvreleq  39437  redundpim3  39465  erALTVeq1  39505  elfunsALTVfunALTV  39533  eldisjsdisj  39575  eldisjeq  39592  disjsuc  39610  parteq1  39628  parteq2  39629  islshpsm  39856  lcvexchlem1  39910  opcon1b  40074  isat3  40183  glbconN  40253  cdleme32fva  41313  cdlemg2cex  41467  dibelval3  42023  dib1dim  42041  doch11  42249  dochsordN  42250  mapdordlem1a  42510  mapd11  42515  mapdsord  42531  mapdcnv11N  42535  mapd0  42541  sn-iotalem  43094  ricfld  43415  fimgmcyc  43419  fsuppind  43439  mrefg2  43555  jm2.23  43840  wepwsolem  43886  dnwech  43892  islssfg2  43915  gicabl  43943  onsupmaxb  44083  onsupeqnmax  44091  orddif0suc  44112  oadif1lem  44223  oadif1  44224  fzunt  44298  fzuntd  44299  fzunt1d  44300  fzuntgd  44301  ifpbi2  44310  ifpbi3  44311  ifpbi1  44320  ifpbi12  44331  ifpbi13  44332  ontric3g  44365  pwinfig  44404  inintabd  44422  cnvcnvintabd  44443  cnvintabd  44446  intimag  44499  briunov2  44525  heeq12  44619  sbcheg  44622  uneqsn  44868  ntrneineine0lem  44926  ntrneineine1lem  44927  ntrneik2  44935  ntrneix2  44936  ntrneik13  44941  ntrneix13  44942  ralbidar  45271  rexbidar  45272  trsbc  45366  relpeq1  45770  relpeq2  45771  relpeq3  45772  relpeq4  45773  relpeq5  45774  n0abso  45802  modelaxreplem3  45806  iindif2f  45995  rnmptpr  46012  iccintsng  46356  xlimres  46652  fsetsniunop  47940  fsetsnprcnex  47946  fcoresf1ob  47964  f1cof1b  47968  f1ocof1ob  47972  dfateq12d  48017  aov0nbovbi  48086  fnotaovb  48089  ichbidv  48356  sprsymrelf  48398  prprsprreu  48422  prprreueq  48423  nprmmul1  48430  edgusgrclnbfin  48761  dfclnbgr6  48775  dfnbgr6  48776  isubgredg  48785  gpgnbgrvtx0  48993  gpgnbgrvtx1  48994  rngcsectALTV  49193  ringcsectALTV  49227  lindslinindsimp2lem5  49395  xpco2  49788  opndisj  49832  i0oii  49849  io1ii  49850  iscnrm3lem2  49864  uobffth  50147  uobeqw  50148  thincpropd  50371  termcpropd  50432  alsbid  50734