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  916  orbi1d  917  ifpbi123d  1079  3orbi123d  1438  3anbi123d  1439  nanbi1  1503  nanbi2  1504  xorbi12d  1527  hadbi123d  1597  had0  1606  cadbi123d  1612  nfbiit  1853  nfbidv  1924  sbequ  2089  nfbidf  2232  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  3156  rexbidv2  3157  r19.21t  3231  r19.23t  3233  rexbida  3249  rexeq  3291  cbvraldva2  3313  raleqf  3318  ralcom2  3339  rmobidva  3355  reubidva  3356  rmobida  3365  reubida  3366  rmoeq1  3373  reueq1  3374  reueqbidv  3378  rmoeq1f  3379  reueq1f  3380  dfsbcq  3730  sbceqbid  3735  sbcbid  3783  sbcbi2  3787  eqsbc2  3792  sbcrext  3811  sbcabel  3816  ralss  3996  rexss  3997  psseq1  4030  psseq2  4031  ssconb  4082  uneq1  4101  difin2  4241  rcompleq  4245  reuun2  4265  sbcnel12g  4354  sbnfc2  4379  reldisj  4393  undif4  4407  disjssun  4408  pssdifcom1  4429  pssdifcom2  4430  sbcssg  4461  eltpg  4630  raltpg  4642  rextpg  4643  r19.12sn  4664  intmin4  4919  dfiun2g  4972  iindif1  5017  iindif2  5019  iinin2  5020  disjprg  5081  disjxun  5083  breq  5087  breq1  5088  breq2  5089  treq  5199  reusv2lem5  5344  rexxfrd  5351  rexxfr2d  5353  rexxfrd2  5355  rabxfrd  5359  opthg2  5432  oteqex2  5453  oteqex  5454  poeq1  5542  soeq1  5560  freq1  5598  weeq1  5618  weeq2  5619  opthprc  5695  wesn  5720  releq  5733  sbcrel  5737  eqrel  5740  eqrelrel  5753  xpiindi  5790  dmopab2rex  5872  dfres3  5949  brres  5951  resieq  5955  dmsnopg  6177  dfco2a  6210  dfpo2  6260  ordeq  6330  limeq  6335  ordunisssuc  6431  iotaeq  6466  sniota  6489  sbcfung  6522  imadif  6582  fneq1  6589  fneq2  6590  feq1  6646  feq2  6647  feq3  6648  sbcfng  6665  sbcfg  6666  f1eq1  6731  f1eq2  6732  f1eq3  6733  foeq1  6748  foeq2  6749  foeq3  6750  f1oeq1  6768  f1oeq2  6769  f1oeq3  6770  mpteqb  6967  rexrnmptw  7047  rexrnmpt  7049  dffo3  7054  dffo3f  7058  fmptco  7082  rexima  7193  dff13  7209  f1imaeq  7220  f1imapss  7221  cbvexfo  7245  f1eqcocnv  7256  fliftcnv  7266  isoeq1  7272  isoeq2  7273  isoeq3  7274  isoeq4  7275  isoeq5  7276  isomin  7292  isowe  7304  eqfunresadj  7315  imaeqsalvOLD  7319  nfriotadw  7332  mpoeq123  7439  rexrnmpo  7507  iunpw  7725  tfinds  7811  resf1extb  7885  fiun  7896  f1iun  7897  opiota  8012  xpord3pred  8102  ottpos  8186  dmtpos  8188  onoviun  8283  smoeq  8290  smoiso2  8309  tfr2b  8335  oarec  8497  oeeui  8538  nnacan  8564  nnmcan  8570  ereq1  8651  ereq2  8652  elecg  8688  ereldm  8697  ixpiin  8872  boxriin  8888  boxcutc  8889  omxpenlem  9016  enfiALT  9122  nnsdomo  9153  isfinite2  9208  ixpfi2  9260  elfi2  9327  fipwss  9342  ttrclse  9648  ennum  9871  cardsdom2  9912  aleph11  10006  alephiso  10020  fin23lem26  10247  compssiso  10296  isf34lem4  10299  isfin5-2  10313  fin1a2lem5  10326  brdom7disj  10453  brdom6disj  10454  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  genpass  10932  ltasr  11023  axpre-lttri  11088  infm3  12115  creur  12153  eqreznegel  12884  rpneg  12976  ltxr  13066  icoshftf1o  13427  elfzm11  13549  elfzomelpfzo  13727  nn0ennn  13941  nnesq  14189  hashbclem  14414  hashf1lem1  14417  leiso  14421  fz1isolem  14423  pr2pwpr  14441  repsdf2  14740  dfrtrclrec2  15020  rexfiuz  15310  cau4  15319  ello1mpt2  15484  o1lo1  15499  fsumcom2  15736  incexc2  15803  fprodcom2  15949  dvdsflip  16286  bitsmod  16405  bitscmp  16407  smueqlem  16459  divgcdcoprm0  16634  hashdvds  16745  prmreclem2  16888  vdwapun  16945  vdwmc2  16950  imasaddfnlem  17492  comfeq  17672  oppcsect  17745  funcres2b  17864  funcpropd  17869  fullpropd  17889  fthpropd  17890  fthres2b  17899  fthres2c  17900  fullres2c  17908  ffthres2c  17909  fucsect  17942  fucinv  17943  setcsect  18056  pospropd  18291  tosso  18383  odulatb  18400  oduclatb  18473  odudlatb  18491  isipodrs  18503  mgmhmpropd  18666  issgrpv  18689  issgrpn0  18690  mndpropd  18727  mhmpropd  18760  issubm2  18772  efmnd1bas  18861  grppropd  18927  grpinvcnv  18982  conjghm  19224  conjnmzb  19228  ghmpropd  19231  gapm  19281  symg1bas  19366  pmtrfrn  19433  cmnpropd  19766  ablpropd  19767  eqgabl  19809  gsumcom2  19950  dmdprd  19975  dprdw  19987  subgdmdprd  20011  pgpfac1lem2  20052  pgpfac1lem4  20055  rngpropd  20155  ringpropd  20269  crngpropd  20270  crngunit  20358  unitpropd  20397  isnirred  20400  nzrpropd  20497  issubrng  20524  subrngpropd  20545  resrhm2b  20579  subrgpropd  20585  rhmpropd  20586  rngcsect  20613  ringcsect  20647  isdomn3  20692  drngpropd  20746  fldpropd  20747  fiidomfld  20751  acsfn1p  20776  abvpropd  20812  lmodprop2d  20919  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  lmhmlvec  21105  lvecprop2d  21164  lvecpropd  21165  df2idl2rng  21254  pzriprnglem10  21470  phlpropd  21635  assapropd  21851  psrbagconf1o  21909  mplmonmul  22014  ismhp3  22108  mat1dimbas  22437  tpspropd  22903  tgss2  22952  lmbr2  23224  ist1-2  23312  ist1-3  23314  subislly  23446  dissnlocfin  23494  iskgen3  23514  txcnmpt  23589  hausdiag  23610  hauseqlcld  23611  xkococnlem  23624  tgqtop  23677  txhmeo  23768  uffix2  23889  ufildr  23896  txflf  23971  tgphaus  24082  qustgplem  24086  qustgphaus  24088  xpsdsval  24346  blin  24386  blres  24396  xmeterval  24397  xmspropd  24438  mspropd  24439  setsms  24445  metequiv  24474  metustsym  24520  restmetu  24535  ngppropd  24602  xrtgioo  24772  metdsge  24815  icopnfcnv  24909  iccpnfcnv  24911  lmhmclm  25054  lmmbr  25225  equivcmet  25284  cmspropd  25316  iunmbl2  25524  ioombl1lem4  25528  mbfaddlem  25627  i1fmullem  25661  itg1mulc  25671  iblcnlem1  25755  iblrelem  25758  iblre  25761  iblcn  25766  limcun  25862  mvth  25959  ofmulrt  26248  resinf1o  26500  quad2  26803  1cubr  26806  dcubic  26810  wilthlem2  27032  dvdsflf1o  27150  dvdsflsumcom  27151  fsumvma  27176  vmasum  27179  logfac2  27180  logfaclbnd  27185  dchrelbas3  27201  lgsquadlem1  27343  lgsquadlem2  27344  eqcuts2  27778  mulsrid  28105  z12sge0  28475  readdscl  28491  ax5seg  29007  ushgredgedg  29298  ushgredgedgloop  29300  nbumgrvtx  29415  upgriswlk  29709  wspniunwspnon  29991  rusgrnumwwlkb0  30042  isclwwlknx  30106  clwwlknscsh  30132  clwwlknonel  30165  0trl  30192  0spth  30196  0clwlk  30200  0crct  30203  0cycl  30204  eupth2lem2  30289  eucrct2eupth  30315  fusgr2wsp2nb  30404  ocin  31367  chpsscon3  31574  chscllem2  31709  adjval  31961  pjimai  32247  mdsldmd1i  32402  elat2  32411  mdsymi  32482  sbceqbidf  32556  rmoxfrd  32562  rmounid  32564  disjxun0  32644  disjrdx  32661  eqrelrd2  32689  fmptcof2  32730  ofpreima  32738  funcnv5mpt  32740  ressupprn  32763  1stpreima  32780  2ndpreima  32781  fpwrelmapffslem  32805  cntrval2  33232  domnpropd  33338  idompropd  33339  subsdrg  33359  qsxpid  33422  grplsm0l  33463  opprlidlabs  33545  ressply1mon1p  33628  psrmonmul  33694  algextdeglem6  33866  smatrcl  33940  locfinreflem  33984  zarcls  34018  zhmnrg  34109  qqhval2  34126  ismntop  34170  reprsuc  34759  reprdifc  34771  bnj919  34910  bnj956  34919  bnj976  34920  bnj1366  34971  bnj916  35075  satfvsucsuc  35547  satfdm  35551  dmopab3rexdif  35587  rexxfr3dALT  35821  sscoid  36093  dfrdg4  36133  altopthbg  36150  broutsideof3  36308  rmoeqbidv  36395  sbequbidv  36396  disjeq12dv  36397  ixpeq12dv  36398  cbvmodavw  36432  cbveudavw  36433  cbvrmodavw  36434  cbvreudavw  36435  cbvsbdavw  36436  cbvsbdavw2  36437  cbvabdavw  36438  cbvsbcdavw  36439  cbvsbcdavw2  36440  cbvdisjdavw  36450  cbvrmodavw2  36465  cbvreudavw2  36466  cbvdisjdavw2  36471  bj-nnfbi  37044  bj-cbvexdv  37107  bj-sbievw  37154  mobidvALT  37164  bj-axreprepsep  37382  bj-restuni  37409  bj-elid6  37484  cbveud  37688  cbvreud  37689  exrecfnlem  37695  wl-ifp-ncond2  37781  wl-ifpimpr  37782  wl-3xorbi123d  37791  wl-sb8eut  37903  wl-sb8eutv  37904  wl-sb8mot  37905  wl-sb8motv  37906  wl-clabtv  37911  wl-clabt  37912  wl-eujustlem1  37913  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem25  37966  ftc1anclem5  38018  istotbnd3  38092  sstotbnd  38096  heibor  38142  isass  38167  isidlc  38336  smprngopr  38373  brvvdif  38589  elecALTV  38592  eqrel2  38626  dmecd  38631  relcnveq2  38650  eldmxrncnvepres  38755  eldmxrncnvepres2  38756  extssr  38910  elrefrelsrel  38921  refreleq  38922  elcnvrefrelsrel  38937  elrelscnveq2  38950  elsymrelsrel  38962  symreleq  38963  eltrrelsrel  38986  trreleq  38987  eleqvrelsrel  38999  eqvreleq  39007  redundpim3  39035  erALTVeq1  39075  elfunsALTVfunALTV  39103  eldisjsdisj  39145  eldisjeq  39162  disjsuc  39180  parteq1  39198  parteq2  39199  islshpsm  39426  lcvexchlem1  39480  opcon1b  39644  isat3  39753  glbconN  39823  cdleme32fva  40883  cdlemg2cex  41037  dibelval3  41593  dib1dim  41611  doch11  41819  dochsordN  41820  mapdordlem1a  42080  mapd11  42085  mapdsord  42101  mapdcnv11N  42105  mapd0  42111  sn-iotalem  42662  ricfld  42975  fimgmcyc  42979  fsuppind  43023  mrefg2  43139  jm2.23  43424  wepwsolem  43470  dnwech  43476  islssfg2  43499  gicabl  43527  onsupmaxb  43667  onsupeqnmax  43675  orddif0suc  43696  oadif1lem  43807  oadif1  43808  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  ifpbi2  43894  ifpbi3  43895  ifpbi1  43904  ifpbi12  43915  ifpbi13  43916  ontric3g  43949  pwinfig  43988  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  intimag  44083  briunov2  44109  heeq12  44203  sbcheg  44206  uneqsn  44452  ntrneineine0lem  44510  ntrneineine1lem  44511  ntrneik2  44519  ntrneix2  44520  ntrneik13  44525  ntrneix13  44526  ralbidar  44871  rexbidar  44872  trsbc  44967  relpeq1  45371  relpeq2  45372  relpeq3  45373  relpeq4  45374  relpeq5  45375  n0abso  45403  modelaxreplem3  45407  iindif2f  45590  rnmptpr  45607  iccintsng  45953  xlimres  46249  fsetsniunop  47497  fsetsnprcnex  47503  fcoresf1ob  47521  f1cof1b  47525  f1ocof1ob  47529  dfateq12d  47574  aov0nbovbi  47643  fnotaovb  47646  ichbidv  47913  sprsymrelf  47955  prprsprreu  47979  prprreueq  47980  nprmmul1  47987  edgusgrclnbfin  48318  dfclnbgr6  48332  dfnbgr6  48333  isubgredg  48342  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  rngcsectALTV  48751  ringcsectALTV  48785  lindslinindsimp2lem5  48938  xpco2  49332  opndisj  49378  i0oii  49395  io1ii  49396  iscnrm3lem2  49410  uobffth  49693  uobeqw  49694  thincpropd  49917  termcpropd  49978