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  1502  nanbi2  1503  xorbi12d  1526  hadbi123d  1596  had0  1605  cadbi123d  1611  nfbiit  1852  nfbidv  1923  sbequ  2088  nfbidf  2231  drex1v  2374  drnf1v  2375  drex1  2445  drnf1  2447  sb4b  2479  drsb1  2499  eujustALT  2572  eubi  2584  eleq1ab  2716  eqeq1d  2738  eqeq1dALT  2739  eqeq2d  2747  abbi  2801  eleq1w  2819  eleq2w  2820  eleq1d  2821  eleq2d  2822  eleq2dALT  2823  eqabdv  2869  nfceqdf  2894  drnfc1  2918  drnfc2  2919  neleq12d  3041  ralbidv2  3155  rexbidv2  3156  r19.21t  3230  r19.23t  3232  rexbida  3248  rexeq  3292  raleqbidvvOLD  3305  cbvraldva2  3318  raleqf  3325  rexeqfOLD  3327  ralcom2  3347  rmobidva  3363  reubidva  3364  rmobida  3373  reubida  3374  rmoeq1  3381  reueq1  3382  rmoeq1OLD  3383  reueq1OLD  3384  reueqbidv  3388  rmoeq1f  3389  reueq1f  3390  dfsbcq  3742  sbceqbid  3747  sbcbid  3795  sbcbi2  3799  eqsbc2  3804  sbcrext  3823  sbcabel  3828  ralss  4008  rexss  4009  psseq1  4042  psseq2  4043  ssconb  4094  uneq1  4113  difin2  4253  rcompleq  4257  reuun2  4277  sbcnel12g  4366  sbnfc2  4391  reldisj  4405  undif4  4419  disjssun  4420  pssdifcom1  4442  pssdifcom2  4443  sbcssg  4474  eltpg  4643  raltpg  4655  rextpg  4656  r19.12sn  4677  intmin4  4932  dfiun2g  4985  iindif1  5030  iindif2  5032  iinin2  5033  disjprg  5094  disjxun  5096  breq  5100  breq1  5101  breq2  5102  treq  5212  reusv2lem5  5347  rexxfrd  5354  rexxfr2d  5356  rexxfrd2  5358  rabxfrd  5362  opthg2  5427  oteqex2  5447  oteqex  5448  poeq1  5535  soeq1  5553  freq1  5591  weeq1  5611  weeq2  5612  opthprc  5688  wesn  5713  releq  5726  sbcrel  5730  eqrel  5733  eqrelrel  5746  xpiindi  5784  dmopab2rex  5866  dfres3  5943  brres  5945  resieq  5949  dmsnopg  6171  dfco2a  6204  dfpo2  6254  ordeq  6324  limeq  6329  ordunisssuc  6425  iotaeq  6460  sniota  6483  sbcfung  6516  imadif  6576  fneq1  6583  fneq2  6584  feq1  6640  feq2  6641  feq3  6642  sbcfng  6659  sbcfg  6660  f1eq1  6725  f1eq2  6726  f1eq3  6727  foeq1  6742  foeq2  6743  foeq3  6744  f1oeq1  6762  f1oeq2  6763  f1oeq3  6764  mpteqb  6960  rexrnmptw  7040  rexrnmpt  7042  dffo3  7047  dffo3f  7051  fmptco  7074  rexima  7184  dff13  7200  f1imaeq  7211  f1imapss  7212  cbvexfo  7236  f1eqcocnv  7247  fliftcnv  7257  isoeq1  7263  isoeq2  7264  isoeq3  7265  isoeq4  7266  isoeq5  7267  isomin  7283  isowe  7295  eqfunresadj  7306  imaeqsalvOLD  7310  nfriotadw  7323  mpoeq123  7430  rexrnmpo  7498  iunpw  7716  tfinds  7802  resf1extb  7876  fiun  7887  f1iun  7888  opiota  8003  xpord3pred  8094  ottpos  8178  dmtpos  8180  onoviun  8275  smoeq  8282  smoiso2  8301  tfr2b  8327  oarec  8489  oeeui  8530  nnacan  8556  nnmcan  8562  ereq1  8643  ereq2  8644  elecg  8680  ereldm  8689  ixpiin  8864  boxriin  8880  boxcutc  8881  omxpenlem  9008  enfiALT  9114  nnsdomo  9145  isfinite2  9200  ixpfi2  9252  elfi2  9319  fipwss  9334  ttrclse  9638  ennum  9861  cardsdom2  9902  aleph11  9996  alephiso  10010  fin23lem26  10237  compssiso  10286  isf34lem4  10289  isfin5-2  10303  fin1a2lem5  10316  brdom7disj  10443  brdom6disj  10444  fpwwe2lem7  10550  fpwwe2lem11  10554  fpwwe2lem12  10555  genpass  10922  ltasr  11013  axpre-lttri  11078  infm3  12103  creur  12141  eqreznegel  12849  rpneg  12941  ltxr  13031  icoshftf1o  13392  elfzm11  13513  elfzomelpfzo  13690  nn0ennn  13904  nnesq  14152  hashbclem  14377  hashf1lem1  14380  leiso  14384  fz1isolem  14386  pr2pwpr  14404  repsdf2  14703  dfrtrclrec2  14983  rexfiuz  15273  cau4  15282  ello1mpt2  15447  o1lo1  15462  fsumcom2  15699  incexc2  15763  fprodcom2  15909  dvdsflip  16246  bitsmod  16365  bitscmp  16367  smueqlem  16419  divgcdcoprm0  16594  hashdvds  16704  prmreclem2  16847  vdwapun  16904  vdwmc2  16909  imasaddfnlem  17451  comfeq  17631  oppcsect  17704  funcres2b  17823  funcpropd  17828  fullpropd  17848  fthpropd  17849  fthres2b  17858  fthres2c  17859  fullres2c  17867  ffthres2c  17868  fucsect  17901  fucinv  17902  setcsect  18015  pospropd  18250  tosso  18342  odulatb  18359  oduclatb  18432  odudlatb  18450  isipodrs  18462  mgmhmpropd  18625  issgrpv  18648  issgrpn0  18649  mndpropd  18686  mhmpropd  18719  issubm2  18731  efmnd1bas  18820  grppropd  18883  grpinvcnv  18938  conjghm  19180  conjnmzb  19184  ghmpropd  19187  gapm  19237  symg1bas  19322  pmtrfrn  19389  cmnpropd  19722  ablpropd  19723  eqgabl  19765  gsumcom2  19906  dmdprd  19931  dprdw  19943  subgdmdprd  19967  pgpfac1lem2  20008  pgpfac1lem4  20011  rngpropd  20111  ringpropd  20225  crngpropd  20226  crngunit  20316  unitpropd  20355  isnirred  20358  nzrpropd  20455  issubrng  20482  subrngpropd  20503  resrhm2b  20537  subrgpropd  20543  rhmpropd  20544  rngcsect  20571  ringcsect  20605  isdomn3  20650  drngpropd  20704  fldpropd  20705  fiidomfld  20709  acsfn1p  20734  abvpropd  20770  lmodprop2d  20877  lsspropd  20971  lmhmpropd  21027  lbspropd  21053  lmhmlvec  21064  lvecprop2d  21123  lvecpropd  21124  df2idl2rng  21213  pzriprnglem10  21447  phlpropd  21612  assapropd  21829  psrbagconf1o  21887  mplmonmul  21993  ismhp3  22087  mat1dimbas  22418  tpspropd  22884  tgss2  22933  lmbr2  23205  ist1-2  23293  ist1-3  23295  subislly  23427  dissnlocfin  23475  iskgen3  23495  txcnmpt  23570  hausdiag  23591  hauseqlcld  23592  xkococnlem  23605  tgqtop  23658  txhmeo  23749  uffix2  23870  ufildr  23877  txflf  23952  tgphaus  24063  qustgplem  24067  qustgphaus  24069  xpsdsval  24327  blin  24367  blres  24377  xmeterval  24378  xmspropd  24419  mspropd  24420  setsms  24426  metequiv  24455  metustsym  24501  restmetu  24516  ngppropd  24583  xrtgioo  24753  metdsge  24796  icopnfcnv  24898  iccpnfcnv  24900  lmhmclm  25045  lmmbr  25216  equivcmet  25275  cmspropd  25307  iunmbl2  25516  ioombl1lem4  25520  mbfaddlem  25619  i1fmullem  25653  itg1mulc  25663  iblcnlem1  25747  iblrelem  25750  iblre  25753  iblcn  25758  limcun  25854  mvth  25955  ofmulrt  26247  resinf1o  26503  quad2  26807  1cubr  26810  dcubic  26814  wilthlem2  27037  dvdsflf1o  27155  dvdsflsumcom  27156  fsumvma  27182  vmasum  27185  logfac2  27186  logfaclbnd  27191  dchrelbas3  27207  lgsquadlem1  27349  lgsquadlem2  27350  eqcuts2  27784  mulsrid  28111  z12sge0  28481  readdscl  28497  ax5seg  29013  ushgredgedg  29304  ushgredgedgloop  29306  nbumgrvtx  29421  upgriswlk  29716  wspniunwspnon  29998  rusgrnumwwlkb0  30049  isclwwlknx  30113  clwwlknscsh  30139  clwwlknonel  30172  0trl  30199  0spth  30203  0clwlk  30207  0crct  30210  0cycl  30211  eupth2lem2  30296  eucrct2eupth  30322  fusgr2wsp2nb  30411  ocin  31373  chpsscon3  31580  chscllem2  31715  adjval  31967  pjimai  32253  mdsldmd1i  32408  elat2  32417  mdsymi  32488  sbceqbidf  32563  rmoxfrd  32569  rmounid  32571  disjxun0  32651  disjrdx  32668  eqrelrd2  32696  fmptcof2  32737  ofpreima  32745  funcnv5mpt  32748  ressupprn  32771  1stpreima  32788  2ndpreima  32789  fpwrelmapffslem  32813  cntrval2  33255  domnpropd  33361  idompropd  33362  subsdrg  33382  qsxpid  33445  grplsm0l  33486  opprlidlabs  33568  ressply1mon1p  33651  algextdeglem6  33881  smatrcl  33955  locfinreflem  33999  zarcls  34033  zhmnrg  34124  qqhval2  34141  ismntop  34185  reprsuc  34774  reprdifc  34786  bnj919  34925  bnj956  34934  bnj976  34935  bnj1366  34987  bnj916  35091  satfvsucsuc  35561  satfdm  35565  dmopab3rexdif  35601  rexxfr3dALT  35835  sscoid  36107  dfrdg4  36147  altopthbg  36164  broutsideof3  36322  rmoeqbidv  36409  sbequbidv  36410  disjeq12dv  36411  ixpeq12dv  36412  cbvmodavw  36446  cbveudavw  36447  cbvrmodavw  36448  cbvreudavw  36449  cbvsbdavw  36450  cbvsbdavw2  36451  cbvabdavw  36452  cbvsbcdavw  36453  cbvsbcdavw2  36454  cbvdisjdavw  36464  cbvrmodavw2  36479  cbvreudavw2  36480  cbvdisjdavw2  36485  bj-nnfbi  36928  bj-cbvexdv  37003  bj-sbievw  37050  mobidvALT  37060  bj-restuni  37304  bj-elid6  37377  cbveud  37579  cbvreud  37580  exrecfnlem  37586  wl-ifp-ncond2  37672  wl-ifpimpr  37673  wl-3xorbi123d  37682  wl-sb8eut  37785  wl-sb8eutv  37786  wl-sb8mot  37787  wl-sb8motv  37788  wl-clabtv  37793  wl-clabt  37794  wl-eujustlem1  37795  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem25  37848  ftc1anclem5  37900  istotbnd3  37974  sstotbnd  37978  heibor  38024  isass  38049  isidlc  38218  smprngopr  38255  brvvdif  38466  elecALTV  38469  eqrel2  38503  dmecd  38508  relcnveq2  38527  eldmxrncnvepres  38632  eldmxrncnvepres2  38633  extssr  38784  elrefrelsrel  38795  refreleq  38796  elcnvrefrelsrel  38811  elrelscnveq2  38824  elsymrelsrel  38836  symreleq  38837  eltrrelsrel  38860  trreleq  38861  eleqvrelsrel  38873  eqvreleq  38881  redundpim3  38909  erALTVeq1  38950  elfunsALTVfunALTV  38978  eldisjsdisj  39008  eldisjeq  39022  disjsuc  39040  parteq1  39055  parteq2  39056  islshpsm  39262  lcvexchlem1  39316  opcon1b  39480  isat3  39589  glbconN  39659  cdleme32fva  40719  cdlemg2cex  40873  dibelval3  41429  dib1dim  41447  doch11  41655  dochsordN  41656  mapdordlem1a  41916  mapd11  41921  mapdsord  41937  mapdcnv11N  41941  mapd0  41947  sn-iotalem  42499  ricfld  42806  fimgmcyc  42810  fsuppind  42854  mrefg2  42970  jm2.23  43259  wepwsolem  43305  dnwech  43311  islssfg2  43334  gicabl  43362  onsupmaxb  43502  onsupeqnmax  43510  orddif0suc  43531  oadif1lem  43642  oadif1  43643  fzunt  43717  fzuntd  43718  fzunt1d  43719  fzuntgd  43720  ifpbi2  43729  ifpbi3  43730  ifpbi1  43739  ifpbi12  43750  ifpbi13  43751  ontric3g  43784  pwinfig  43823  inintabd  43841  cnvcnvintabd  43862  cnvintabd  43865  intimag  43918  briunov2  43944  heeq12  44038  sbcheg  44041  uneqsn  44287  ntrneineine0lem  44345  ntrneineine1lem  44346  ntrneik2  44354  ntrneix2  44355  ntrneik13  44360  ntrneix13  44361  ralbidar  44706  rexbidar  44707  trsbc  44802  relpeq1  45206  relpeq2  45207  relpeq3  45208  relpeq4  45209  relpeq5  45210  n0abso  45238  modelaxreplem3  45242  iindif2f  45425  rnmptpr  45442  iccintsng  45790  xlimres  46086  fsetsniunop  47316  fsetsnprcnex  47322  fcoresf1ob  47340  f1cof1b  47344  f1ocof1ob  47348  dfateq12d  47393  aov0nbovbi  47462  fnotaovb  47465  ichbidv  47720  sprsymrelf  47762  prprsprreu  47786  prprreueq  47787  edgusgrclnbfin  48109  dfclnbgr6  48123  dfnbgr6  48124  isubgredg  48133  gpgnbgrvtx0  48341  gpgnbgrvtx1  48342  rngcsectALTV  48542  ringcsectALTV  48576  lindslinindsimp2lem5  48729  xpco2  49123  opndisj  49169  i0oii  49186  io1ii  49187  iscnrm3lem2  49201  uobffth  49484  uobeqw  49485  thincpropd  49708  termcpropd  49769