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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi1d  346  pm5.32rd  588  orbi2d  928  orbi1d  929  ifpbi123d  1093  3orbi123d  1461  3anbi123d  1462  nanbi1  1528  nanbi2  1529  xorbi12d  1552  hadbi123d  1622  had0  1631  cadbi123d  1637  nfbiit  1878  nfbidv  1949  sbequ  2123  nfbidf  2266  drex1v  2408  drnf1v  2409  drex1  2479  drnf1  2481  sb4b  2513  drsb1  2533  eujustALT  2606  eubi  2618  eleq1ab  2749  eqeq1d  2771  eqeq1dALT  2772  eqeq2d  2780  abbi  2834  eleq1w  2852  eleq2w  2853  eleq1d  2854  eleq2d  2855  eleq2dALT  2856  eqabdv  2902  nfceqdf  2927  drnfc1  2950  drnfc2  2951  neleq12d  3075  ralbidv2  3190  rexbidv2  3191  r19.21t  3265  r19.23t  3267  rexbida  3283  rexeq  3325  cbvraldva2  3347  raleqf  3352  ralcom2  3373  rmobidva  3389  reubidva  3390  rmobida  3399  reubida  3400  rmoeq1  3407  reueq1  3408  reueqbidv  3412  rmoeq1f  3413  reueq1f  3414  dfsbcq  3755  sbceqbid  3760  sbcbid  3807  sbcbi2  3811  eqsbc2  3816  sbcrext  3835  sbcabel  3840  ralss  4018  rexss  4019  psseq1  4052  psseq2  4053  ssconb  4104  uneq1  4123  difin2  4262  rcompleq  4266  reuun2  4286  sbcnel12g  4385  sbnfc2  4410  reldisj  4419  undif4  4433  disjssun  4434  pssdifcom1  4455  pssdifcom2  4456  sbcssg  4487  eltpg  4657  raltpg  4669  rextpg  4670  r19.12sn  4691  intmin4  4946  dfiun2g  4998  iindif1  5045  iindif2  5047  iinin2  5048  disjprg  5109  disjxun  5111  breq  5115  breq1  5116  breq2  5117  treq  5229  reusv2lem5  5374  rexxfrd  5381  rexxfr2d  5383  rexxfrd2  5385  rabxfrd  5389  opthg2  5462  oteqex2  5483  oteqex  5484  poeq1  5573  soeq1  5591  freq1  5629  weeq1  5649  weeq2  5650  opthprc  5726  wesn  5751  releq  5764  sbcrel  5768  eqrel  5771  eqrelrel  5784  xpiindi  5822  dmopab2rex  5908  dfres3  5984  brres  5986  resieq  5990  dmsnopg  6215  dfco2a  6248  dfpo2  6298  ordeq  6368  limeq  6373  ordunisssuc  6470  iotaeq  6505  sniota  6528  sbcfung  6561  imadif  6621  fneq1  6627  fneq2  6628  feq1  6684  feq2  6685  feq3  6686  sbcfng  6703  sbcfg  6704  f1eq1  6770  f1eq2  6771  f1eq3  6772  foeq1  6789  foeq2  6790  foeq3  6791  f1oeq1  6809  f1oeq2  6810  f1oeq3  6811  mpteqb  7010  rexrnmptw  7091  rexrnmpt  7093  dffo3  7098  dffo3f  7102  fmptco  7126  rexima  7237  dff13  7253  f1imaeq  7264  f1imapss  7265  cbvexfo  7289  f1eqcocnv  7300  fliftcnv  7310  isoeq1  7316  isoeq2  7317  isoeq3  7318  isoeq4  7319  isoeq5  7320  isomin  7336  isowe  7348  eqfunresadj  7359  imaeqsalvOLD  7363  nfriotadw  7376  mpoeq123  7483  rexrnmpo  7551  iunpw  7770  tfinds  7856  resf1extb  7931  fiun  7940  f1iun  7941  opiota  8056  xpord3pred  8148  ottpos  8232  dmtpos  8234  onoviun  8330  smoeq  8337  smoiso2  8356  tfr2b  8383  oarec  8547  oeeui  8588  nnacan  8614  nnmcan  8620  ereq1  8702  ereq2  8703  elecg  8739  ereldm  8748  ixpiin  8922  boxriin  8938  boxcutc  8939  omxpenlem  9066  enfiALT  9172  nnsdomo  9203  isfinite2  9258  ixpfi2  9307  elfi2  9374  fipwss  9389  ttrclse  9696  ennum  9933  cardsdom2  9974  aleph11  10068  alephiso  10082  fin23lem26  10309  compssiso  10358  isf34lem4  10361  isfin5-2  10375  fin1a2lem5  10388  brdom7disj  10515  brdom6disj  10516  fpwwe2lem7  10622  fpwwe2lem11  10626  fpwwe2lem12  10627  genpass  10994  ltasr  11085  axpre-lttri  11150  infm3  12174  creur  12212  eqreznegel  12958  rpneg  13050  ltxr  13140  icoshftf1o  13501  elfzm11  13623  elfzomelpfzo  13801  nn0ennn  14015  nnesq  14263  hashbclem  14489  hashf1lem1  14492  leiso  14496  fz1isolem  14498  pr2pwpr  14516  repsdf2  14815  dfrtrclrec2  15095  rexfiuz  15399  cau4  15408  ello1mpt2  15573  o1lo1  15588  fsumcom2  15825  incexc2  15892  fprodcom2  16038  dvdsflip  16375  bitsmod  16494  bitscmp  16496  smueqlem  16548  divgcdcoprm0  16723  hashdvds  16834  prmreclem2  16977  vdwapun  17034  vdwmc2  17039  imasaddfnlem  17582  comfeq  17762  oppcsect  17835  funcres2b  17954  funcpropd  17959  fullpropd  17979  fthpropd  17980  fthres2b  17989  fthres2c  17990  fullres2c  17998  ffthres2c  17999  fucsect  18032  fucinv  18033  setcsect  18146  pospropd  18381  tosso  18473  odulatb  18490  oduclatb  18563  odudlatb  18581  isipodrs  18593  mgmhmpropd  18756  issgrpv  18779  issgrpn0  18780  mndpropd  18817  mhmpropd  18850  issubm2  18862  efmnd1bas  18952  grppropd  19018  grpinvcnv  19073  qsxpid  19243  conjghm  19319  conjnmzb  19323  ghmpropd  19326  gapm  19376  symg1bas  19461  pmtrfrn  19528  cmnpropd  19861  ablpropd  19862  eqgabl  19904  gsumcom2  20045  dmdprd  20070  dprdw  20082  subgdmdprd  20106  pgpfac1lem2  20147  pgpfac1lem4  20150  rngpropd  20252  ringpropd  20371  crngpropd  20372  crngunit  20460  unitpropd  20499  isnirred  20502  nzrpropd  20604  issubrng  20632  subrngpropd  20653  resrhm2b  20687  subrgpropd  20693  rhmpropd  20694  rngcsect  20721  ringcsect  20755  isdomn3  20799  drngpropd  20851  fldpropd  20852  fiidomfld  20856  acsfn1p  20880  abvpropd  20916  lmodprop2d  21023  lsspropd  21116  lmhmpropd  21172  lbspropd  21198  lmhmlvec  21209  lvecprop2d  21268  lvecpropd  21269  df2idl2rng  21366  pzriprnglem10  21609  phlpropd  21774  assapropd  21990  psrbagconf1o  22048  mplmonmul  22156  ismhp3  22274  mat1dimbas  22598  tpspropd  23064  tgss2  23113  lmbr2  23385  ist1-2  23473  ist1-3  23475  subislly  23607  dissnlocfin  23655  iskgen3  23675  txcnmpt  23750  hausdiag  23771  hauseqlcld  23772  xkococnlem  23785  tgqtop  23838  txhmeo  23929  uffix2  24050  ufildr  24057  txflf  24132  tgphaus  24243  qustgplem  24247  qustgphaus  24249  xpsdsval  24507  blin  24547  blres  24557  xmeterval  24558  xmspropd  24599  mspropd  24600  setsms  24606  metequiv  24635  metustsym  24681  restmetu  24696  ngppropd  24763  xrtgioo  24933  metdsge  24976  icopnfcnv  25070  iccpnfcnv  25072  lmhmclm  25215  lmmbr  25386  equivcmet  25445  cmspropd  25477  iunmbl2  25685  ioombl1lem4  25689  mbfaddlem  25788  i1fmullem  25822  itg1mulc  25832  iblcnlem1  25916  iblrelem  25919  iblre  25922  iblcn  25927  limcun  26023  mvth  26120  ofmulrt  26409  resinf1o  26667  quad2  26970  1cubr  26973  dcubic  26977  wilthlem2  27199  dvdsflf1o  27317  dvdsflsumcom  27318  fsumvma  27343  vmasum  27346  logfac2  27347  logfaclbnd  27352  dchrelbas3  27368  lgsquadlem1  27510  lgsquadlem2  27511  eqcuts2  27945  mulsrid  28272  z12sge0  28642  readdscl  28658  elplng  29020  plngcplem  29025  ax5seg  29229  ushgredgedg  29520  ushgredgedgloop  29522  nbumgrvtx  29637  upgriswlk  29931  wspniunwspnon  30213  rusgrnumwwlkb0  30264  isclwwlknx  30328  clwwlknscsh  30354  clwwlknonel  30387  0trl  30414  0spth  30418  0clwlk  30422  0crct  30425  0cycl  30426  eupth2lem2  30511  eucrct2eupth  30537  fusgr2wsp2nb  30626  ocin  31589  chpsscon3  31796  chscllem2  31931  adjval  32183  pjimai  32469  mdsldmd1i  32624  elat2  32633  mdsymi  32704  sbceqbidf  32774  rmoxfrd  32780  rmounid  32782  disjxun0  32860  disjrdx  32877  eqrelrd2  32902  fmptcof2  32943  ofpreima  32951  funcnv5mpt  32953  ressupprn  32976  1stpreima  32993  2ndpreima  32994  fpwrelmapffslem  33018  cntrval2  33432  domnpropd  33541  idompropd  33542  subsdrg  33562  grplsm0l  33656  opprlidlabs  33712  ressply1mon1p  33803  psrmonmul  33885  algextdeglem6  34057  smatrcl  34131  locfinreflem  34175  zarcls  34209  zhmnrg  34300  qqhval2  34317  ismntop  34361  reprsuc  34947  reprdifc  34959  bnj919  35101  bnj956  35110  bnj976  35111  bnj1366  35162  bnj916  35266  satfvsucsuc  35790  satfdm  35794  dmopab3rexdif  35830  rexxfr3dALT  36064  sscoid  36336  dfrdg4  36376  altopthbg  36393  broutsideof3  36551  rmoeqbidv  36648  sbequbidv  36649  disjeq12dv  36650  ixpeq12dv  36651  cbvmodavw  36685  cbveudavw  36686  cbvrmodavw  36687  cbvreudavw  36688  cbvsbdavw  36689  cbvsbdavw2  36690  cbvabdavw  36691  cbvsbcdavw  36692  cbvsbcdavw2  36693  cbvdisjdavw  36703  cbvrmodavw2  36718  cbvreudavw2  36719  cbvdisjdavw2  36724  bj-nnfbi  37295  bj-cbvexdv  37358  bj-sbievw  37405  mobidvALT  37415  bj-axreprepsep  37634  bj-restuni  37661  bj-elid6  37736  cbveud  37940  cbvreud  37941  exrecfnlem  37947  wl-ifp-ncond2  38033  wl-ifpimpr  38034  wl-3xorbi123d  38043  wl-sb8eut  38155  wl-sb8eutv  38156  wl-sb8mot  38157  wl-sb8motv  38158  wl-clabtv  38163  wl-clabt  38164  wl-eujustlem1  38165  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem25  38218  ftc1anclem5  38270  istotbnd3  38344  sstotbnd  38348  heibor  38394  isass  38419  isidlc  38588  smprngopr  38625  brvvdif  38841  elecALTV  38844  eqrel2  38878  dmecd  38883  relcnveq2  38902  eldmxrncnvepres  39007  eldmxrncnvepres2  39008  extssr  39162  elrefrelsrel  39173  refreleq  39174  elcnvrefrelsrel  39189  elrelscnveq2  39202  elsymrelsrel  39214  symreleq  39215  eltrrelsrel  39238  trreleq  39239  eleqvrelsrel  39251  eqvreleq  39259  redundpim3  39287  erALTVeq1  39327  elfunsALTVfunALTV  39355  eldisjsdisj  39397  eldisjeq  39414  disjsuc  39432  parteq1  39450  parteq2  39451  islshpsm  39678  lcvexchlem1  39732  opcon1b  39896  isat3  40005  glbconN  40075  cdleme32fva  41135  cdlemg2cex  41289  dibelval3  41845  dib1dim  41863  doch11  42071  dochsordN  42072  mapdordlem1a  42332  mapd11  42337  mapdsord  42353  mapdcnv11N  42357  mapd0  42363  sn-iotalem  42916  ricfld  43224  fimgmcyc  43228  fsuppind  43248  mrefg2  43364  jm2.23  43649  wepwsolem  43695  dnwech  43701  islssfg2  43724  gicabl  43752  onsupmaxb  43892  onsupeqnmax  43900  orddif0suc  43921  oadif1lem  44032  oadif1  44033  fzunt  44107  fzuntd  44108  fzunt1d  44109  fzuntgd  44110  ifpbi2  44119  ifpbi3  44120  ifpbi1  44129  ifpbi12  44140  ifpbi13  44141  ontric3g  44174  pwinfig  44213  inintabd  44231  cnvcnvintabd  44252  cnvintabd  44255  intimag  44308  briunov2  44334  heeq12  44428  sbcheg  44431  uneqsn  44677  ntrneineine0lem  44735  ntrneineine1lem  44736  ntrneik2  44744  ntrneix2  44745  ntrneik13  44750  ntrneix13  44751  ralbidar  45080  rexbidar  45081  trsbc  45175  relpeq1  45579  relpeq2  45580  relpeq3  45581  relpeq4  45582  relpeq5  45583  n0abso  45611  modelaxreplem3  45615  iindif2f  45804  rnmptpr  45821  iccintsng  46165  xlimres  46461  fsetsniunop  47709  fsetsnprcnex  47715  fcoresf1ob  47733  f1cof1b  47737  f1ocof1ob  47741  dfateq12d  47786  aov0nbovbi  47855  fnotaovb  47858  ichbidv  48125  sprsymrelf  48167  prprsprreu  48191  prprreueq  48192  nprmmul1  48199  edgusgrclnbfin  48530  dfclnbgr6  48544  dfnbgr6  48545  isubgredg  48554  gpgnbgrvtx0  48762  gpgnbgrvtx1  48763  rngcsectALTV  48963  ringcsectALTV  48997  lindslinindsimp2lem5  49161  xpco2  49554  opndisj  49600  i0oii  49617  io1ii  49618  iscnrm3lem2  49632  uobffth  49915  uobeqw  49916  thincpropd  50139  termcpropd  50200  alsbid  50499