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  2084  nfbidf  2225  drex1v  2368  drnf1v  2369  drex1  2439  drnf1  2441  sb4b  2473  drsb1  2493  eujustALT  2565  eubi  2577  eleq1ab  2709  eqeq1d  2731  eqeq1dALT  2732  eqeq2d  2740  abbi  2794  eleq1w  2811  eleq2w  2812  eleq1d  2813  eleq2d  2814  eleq2dALT  2815  eqabdv  2861  nfceqdf  2887  drnfc1  2911  drnfc2  2912  neleq12d  3034  ralbidv2  3152  rexbidv2  3153  r19.21t  3231  r19.23t  3233  rexbida  3249  rexeq  3295  raleqbidvvOLD  3308  cbvraldva2  3321  cbvrexdva2OLD  3323  raleqf  3329  rexeqfOLD  3331  ralcom2  3351  rmobidva  3369  reubidva  3370  rmobida  3379  reubida  3380  rmoeq1  3387  reueq1  3388  rmoeq1OLD  3389  reueq1OLD  3390  reueqbidv  3394  rmoeq1f  3395  reueq1f  3396  dfsbcq  3755  sbceqbid  3760  sbcbid  3808  sbcbi2  3812  eqsbc2  3817  sbcrext  3836  sbcabel  3841  ralss  4021  rexss  4022  psseq1  4053  psseq2  4054  ssconb  4105  uneq1  4124  difin2  4264  rcompleq  4268  reuun2  4288  sbcnel12g  4377  sbnfc2  4402  reldisj  4416  undif4  4430  disjssun  4431  pssdifcom1  4453  pssdifcom2  4454  sbcssg  4483  eltpg  4650  raltpg  4662  rextpg  4663  r19.12sn  4684  intmin4  4941  dfiun2g  4994  dfiun2gOLD  4995  iindif1  5039  iindif2  5041  iinin2  5042  disjprg  5103  disjxun  5105  breq  5109  breq1  5110  breq2  5111  treq  5222  reusv2lem5  5357  rexxfrd  5364  rexxfr2d  5366  rexxfrd2  5368  rabxfrd  5372  opthg2  5439  oteqex2  5459  oteqex  5460  poeq1  5549  soeq1  5567  freq1  5605  weeq1  5625  weeq2  5626  opthprc  5702  wesn  5727  releq  5739  sbcrel  5743  eqrel  5747  eqrelrel  5760  xpiindi  5799  dmopab2rex  5881  dfres3  5955  brres  5957  resieq  5961  dmsnopg  6186  dfco2a  6219  dfpo2  6269  ordeq  6339  limeq  6344  ordunisssuc  6440  iotaeq  6476  sniota  6502  sbcfung  6540  imadif  6600  fneq1  6609  fneq2  6610  feq1  6666  feq2  6667  feq3  6668  sbcfng  6685  sbcfg  6686  f1eq1  6751  f1eq2  6752  f1eq3  6753  foeq1  6768  foeq2  6769  foeq3  6770  f1oeq1  6788  f1oeq2  6789  f1oeq3  6790  mpteqb  6987  rexrnmptw  7067  rexrnmpt  7069  dffo3  7074  dffo3f  7078  fmptco  7101  rexima  7212  dff13  7229  f1imaeq  7240  f1imapss  7241  cbvexfo  7265  f1eqcocnv  7276  fliftcnv  7286  isoeq1  7292  isoeq2  7293  isoeq3  7294  isoeq4  7295  isoeq5  7296  isomin  7312  isowe  7324  eqfunresadj  7335  imaeqsalvOLD  7339  nfriotadw  7352  mpoeq123  7461  rexrnmpo  7529  iunpw  7747  tfinds  7836  resf1extb  7910  fiun  7921  f1iun  7922  opiota  8038  xpord3pred  8131  ottpos  8215  dmtpos  8217  onoviun  8312  smoeq  8319  smoiso2  8338  tfr2b  8364  oarec  8526  oeeui  8566  nnacan  8592  nnmcan  8598  ereq1  8678  ereq2  8679  elecg  8715  ereldm  8724  ixpiin  8897  boxriin  8913  boxcutc  8914  omxpenlem  9042  enfiALT  9152  nnsdomo  9182  isfinite2  9245  ixpfi2  9301  elfi2  9365  fipwss  9380  ttrclse  9680  ennum  9900  cardsdom2  9941  aleph11  10037  alephiso  10051  fin23lem26  10278  compssiso  10327  isf34lem4  10330  isfin5-2  10344  fin1a2lem5  10357  brdom7disj  10484  brdom6disj  10485  fpwwe2lem7  10590  fpwwe2lem11  10594  fpwwe2lem12  10595  genpass  10962  ltasr  11053  axpre-lttri  11118  infm3  12142  creur  12180  eqreznegel  12893  rpneg  12985  ltxr  13075  icoshftf1o  13435  elfzm11  13556  elfzomelpfzo  13732  nn0ennn  13944  nnesq  14192  hashbclem  14417  hashf1lem1  14420  leiso  14424  fz1isolem  14426  pr2pwpr  14444  repsdf2  14743  dfrtrclrec2  15024  rexfiuz  15314  cau4  15323  ello1mpt2  15488  o1lo1  15503  fsumcom2  15740  incexc2  15804  fprodcom2  15950  dvdsflip  16287  bitsmod  16406  bitscmp  16408  smueqlem  16460  divgcdcoprm0  16635  hashdvds  16745  prmreclem2  16888  vdwapun  16945  vdwmc2  16950  imasaddfnlem  17491  comfeq  17667  oppcsect  17740  funcres2b  17859  funcpropd  17864  fullpropd  17884  fthpropd  17885  fthres2b  17894  fthres2c  17895  fullres2c  17903  ffthres2c  17904  fucsect  17937  fucinv  17938  setcsect  18051  pospropd  18286  tosso  18378  odulatb  18393  oduclatb  18466  odudlatb  18484  isipodrs  18496  mgmhmpropd  18625  issgrpv  18648  issgrpn0  18649  mndpropd  18686  mhmpropd  18719  issubm2  18731  efmnd1bas  18820  grppropd  18883  grpinvcnv  18938  conjghm  19181  conjnmzb  19185  ghmpropd  19188  gapm  19238  symg1bas  19321  pmtrfrn  19388  cmnpropd  19721  ablpropd  19722  eqgabl  19764  gsumcom2  19905  dmdprd  19930  dprdw  19942  subgdmdprd  19966  pgpfac1lem2  20007  pgpfac1lem4  20010  rngpropd  20083  ringpropd  20197  crngpropd  20198  crngunit  20287  unitpropd  20326  isnirred  20329  nzrpropd  20429  issubrng  20456  subrngpropd  20477  resrhm2b  20511  subrgpropd  20517  rhmpropd  20518  rngcsect  20545  ringcsect  20579  isdomn3  20624  drngpropd  20678  fldpropd  20679  fiidomfld  20683  acsfn1p  20708  abvpropd  20744  lmodprop2d  20830  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  lmhmlvec  21017  lvecprop2d  21076  lvecpropd  21077  df2idl2rng  21166  pzriprnglem10  21400  phlpropd  21564  assapropd  21781  psrbagconf1o  21838  mplmonmul  21943  ismhp3  22029  mat1dimbas  22359  tpspropd  22825  tgss2  22874  lmbr2  23146  ist1-2  23234  ist1-3  23236  subislly  23368  dissnlocfin  23416  iskgen3  23436  txcnmpt  23511  hausdiag  23532  hauseqlcld  23533  xkococnlem  23546  tgqtop  23599  txhmeo  23690  uffix2  23811  ufildr  23818  txflf  23893  tgphaus  24004  qustgplem  24008  qustgphaus  24010  xpsdsval  24269  blin  24309  blres  24319  xmeterval  24320  xmspropd  24361  mspropd  24362  setsms  24368  metequiv  24397  metustsym  24443  restmetu  24458  ngppropd  24525  xrtgioo  24695  metdsge  24738  icopnfcnv  24840  iccpnfcnv  24842  lmhmclm  24987  lmmbr  25158  equivcmet  25217  cmspropd  25249  iunmbl2  25458  ioombl1lem4  25462  mbfaddlem  25561  i1fmullem  25595  itg1mulc  25605  iblcnlem1  25689  iblrelem  25692  iblre  25695  iblcn  25700  limcun  25796  mvth  25897  ofmulrt  26189  resinf1o  26445  quad2  26749  1cubr  26752  dcubic  26756  wilthlem2  26979  dvdsflf1o  27097  dvdsflsumcom  27098  fsumvma  27124  vmasum  27127  logfac2  27128  logfaclbnd  27133  dchrelbas3  27149  lgsquadlem1  27291  lgsquadlem2  27292  eqscut2  27718  mulsrid  28016  zs12ge0  28342  readdscl  28350  ax5seg  28865  ushgredgedg  29156  ushgredgedgloop  29158  nbumgrvtx  29273  upgriswlk  29569  wspniunwspnon  29853  rusgrnumwwlkb0  29901  isclwwlknx  29965  clwwlknscsh  29991  clwwlknonel  30024  0trl  30051  0spth  30055  0clwlk  30059  0crct  30062  0cycl  30063  eupth2lem2  30148  eucrct2eupth  30174  fusgr2wsp2nb  30263  ocin  31225  chpsscon3  31432  chscllem2  31567  adjval  31819  pjimai  32105  mdsldmd1i  32260  elat2  32269  mdsymi  32340  sbceqbidf  32416  rmoxfrd  32422  rmounid  32424  disjxun0  32503  disjrdx  32520  eqrelrd2  32544  fmptcof2  32581  ofpreima  32589  funcnv5mpt  32592  ressupprn  32613  1stpreima  32630  2ndpreima  32631  fpwrelmapffslem  32655  cntrval2  33128  domnpropd  33227  idompropd  33228  subsdrg  33248  qsxpid  33333  grplsm0l  33374  opprlidlabs  33456  ressply1mon1p  33537  algextdeglem6  33712  smatrcl  33786  locfinreflem  33830  zarcls  33864  zhmnrg  33955  qqhval2  33972  ismntop  34016  reprsuc  34606  reprdifc  34618  bnj919  34757  bnj956  34766  bnj976  34767  bnj1366  34819  bnj916  34923  satfvsucsuc  35352  satfdm  35356  dmopab3rexdif  35392  rexxfr3dALT  35626  sscoid  35901  dfrdg4  35939  altopthbg  35956  broutsideof3  36114  rmoeqbidv  36201  sbequbidv  36202  disjeq12dv  36203  ixpeq12dv  36204  cbvmodavw  36238  cbveudavw  36239  cbvrmodavw  36240  cbvreudavw  36241  cbvsbdavw  36242  cbvsbdavw2  36243  cbvabdavw  36244  cbvsbcdavw  36245  cbvsbcdavw2  36246  cbvdisjdavw  36256  cbvrmodavw2  36271  cbvreudavw2  36272  cbvdisjdavw2  36277  bj-nnfbi  36713  bj-cbvexdv  36788  bj-sbievw  36835  mobidvALT  36845  bj-restuni  37085  bj-elid6  37158  cbveud  37360  cbvreud  37361  exrecfnlem  37367  wl-ifp-ncond2  37453  wl-ifpimpr  37454  wl-3xorbi123d  37463  wl-sb8eut  37566  wl-sb8eutv  37567  wl-sb8mot  37568  wl-sb8motv  37569  wl-clabtv  37585  wl-clabt  37586  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem25  37639  ftc1anclem5  37691  istotbnd3  37765  sstotbnd  37769  heibor  37815  isass  37840  isidlc  38009  smprngopr  38046  brvvdif  38252  elecALTV  38255  eqrel2  38287  dmecd  38292  relcnveq2  38311  eldmxrncnvepres  38396  eldmxrncnvepres2  38397  elrelscnveq2  38484  extssr  38500  elrefrelsrel  38511  refreleq  38512  elcnvrefrelsrel  38527  elsymrelsrel  38548  symreleq  38549  eltrrelsrel  38572  trreleq  38573  eleqvrelsrel  38585  eqvreleq  38593  redundpim3  38621  erALTVeq1  38661  elfunsALTVfunALTV  38689  eldisjsdisj  38719  eldisjeq  38733  disjsuc  38751  parteq1  38766  parteq2  38767  islshpsm  38973  lcvexchlem1  39027  opcon1b  39191  isat3  39300  glbconN  39370  glbconNOLD  39371  cdleme32fva  40431  cdlemg2cex  40585  dibelval3  41141  dib1dim  41159  doch11  41367  dochsordN  41368  mapdordlem1a  41628  mapd11  41633  mapdsord  41649  mapdcnv11N  41653  mapd0  41659  sn-iotalem  42209  ricfld  42518  fimgmcyc  42522  fsuppind  42578  mrefg2  42695  jm2.23  42985  wepwsolem  43031  dnwech  43037  islssfg2  43060  gicabl  43088  onsupmaxb  43228  onsupeqnmax  43236  orddif0suc  43257  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  ifpbi2  43456  ifpbi3  43457  ifpbi1  43466  ifpbi12  43477  ifpbi13  43478  ontric3g  43511  pwinfig  43550  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  intimag  43645  briunov2  43671  heeq12  43765  sbcheg  43768  uneqsn  44014  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneik2  44081  ntrneix2  44082  ntrneik13  44087  ntrneix13  44088  ralbidar  44434  rexbidar  44435  trsbc  44530  relpeq1  44934  relpeq2  44935  relpeq3  44936  relpeq4  44937  relpeq5  44938  n0abso  44966  modelaxreplem3  44970  iindif2f  45154  rnmptpr  45171  iccintsng  45521  xlimres  45819  fsetsniunop  47050  fsetsnprcnex  47056  fcoresf1ob  47074  f1cof1b  47078  f1ocof1ob  47082  dfateq12d  47127  aov0nbovbi  47196  fnotaovb  47199  ichbidv  47454  sprsymrelf  47496  prprsprreu  47520  prprreueq  47521  edgusgrclnbfin  47842  dfclnbgr6  47856  dfnbgr6  47857  isubgredg  47866  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  rngcsectALTV  48263  ringcsectALTV  48297  lindslinindsimp2lem5  48451  xpco2  48845  opndisj  48891  i0oii  48908  io1ii  48909  iscnrm3lem2  48923  uobffth  49207  uobeqw  49208  thincpropd  49431  termcpropd  49492