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  1095  3orbi123d  1463  3anbi123d  1464  nanbi1  1531  nanbi2  1532  xorbi12d  1555  hadbi123d  1625  had0  1634  cadbi123d  1640  nfbiit  1881  nfbidv  1952  sbequ  2117  nfbidf  2260  drex1v  2402  drnf1v  2403  drex1  2473  drnf1  2475  sb4b  2507  drsb1  2527  eujustALT  2600  eubi  2612  eleq1ab  2743  eqeq1d  2765  eqeq1dALT  2766  eqeq2d  2774  abbi  2828  eleq1w  2846  eleq2w  2847  eleq1d  2848  eleq2d  2849  eleq2dALT  2850  eqabdv  2896  nfceqdf  2921  drnfc1  2944  drnfc2  2945  neleq12d  3069  ralbidv2  3184  rexbidv2  3185  r19.21t  3259  r19.23t  3261  rexbida  3277  rexeq  3319  cbvraldva2  3340  raleqf  3345  ralcom2  3366  rmobidva  3382  reubidva  3383  rmobida  3392  reubida  3393  rmoeq1  3400  reueq1  3401  reueqbidv  3405  rmoeq1f  3406  reueq1f  3407  dfsbcq  3746  sbceqbid  3751  sbcbid  3798  sbcbi2  3802  eqsbc2  3807  sbcrext  3826  sbcabel  3831  ralss  4010  rexss  4011  psseq1  4044  psseq2  4045  ssconb  4096  uneq1  4115  difin2  4254  rcompleq  4258  reuun2  4278  sbcnel12g  4379  sbnfc2  4404  reldisj  4413  undif4  4427  disjssun  4428  pssdifcom1  4450  pssdifcom2  4451  sbcssg  4482  eltpg  4652  raltpg  4664  rextpg  4665  r19.12sn  4686  intmin4  4942  dfiun2g  4994  iindif1  5041  iindif2  5043  iinin2  5044  disjprg  5105  disjxun  5107  breq  5111  breq1  5112  breq2  5113  treq  5225  reusv2lem5  5373  rexxfrd  5380  rexxfr2d  5382  rexxfrd2  5384  rabxfrd  5388  opthg2  5461  oteqex2  5482  oteqex  5483  poeq1  5572  soeq1  5590  freq1  5628  weeq1  5648  weeq2  5649  opthprc  5725  wesn  5750  releq  5763  sbcrel  5767  eqrel  5770  eqrelrel  5783  xpiindi  5821  dmopab2rex  5907  dfres3  5983  brres  5985  resieq  5989  dmsnopg  6214  dfco2a  6247  dfpo2  6297  ordeq  6367  limeq  6372  ordunisssuc  6469  iotaeq  6504  sniota  6527  sbcfung  6560  imadif  6620  fneq1  6626  fneq2  6627  feq1  6683  feq2  6684  feq3  6685  sbcfng  6702  sbcfg  6703  f1eq1  6769  f1eq2  6770  f1eq3  6771  foeq1  6788  foeq2  6789  foeq3  6790  f1oeq1  6808  f1oeq2  6809  f1oeq3  6810  mpteqb  7009  rexrnmptw  7090  rexrnmpt  7092  dffo3  7097  dffo3f  7101  fmptco  7125  rexima  7236  dff13  7252  f1imaeq  7263  f1imapss  7264  cbvexfo  7288  f1eqcocnv  7299  fliftcnv  7309  isoeq1  7315  isoeq2  7316  isoeq3  7317  isoeq4  7318  isoeq5  7319  isomin  7335  isowe  7347  eqfunresadj  7358  imaeqsalvOLD  7362  nfriotadw  7375  mpoeq123  7482  rexrnmpo  7550  iunpw  7766  tfinds  7852  resf1extb  7927  fiun  7936  f1iun  7937  opiota  8052  xpord3pred  8144  ottpos  8228  dmtpos  8230  onoviun  8326  smoeq  8333  smoiso2  8352  tfr2b  8379  oarec  8543  oeeui  8584  nnacan  8610  nnmcan  8616  ereq1  8698  ereq2  8699  elecg  8735  ereldm  8744  ixpiin  8918  boxriin  8934  boxcutc  8935  omxpenlem  9062  enfiALT  9168  nnsdomo  9199  isfinite2  9254  ixpfi2  9303  elfi2  9370  fipwss  9385  ttrclse  9692  ennum  9929  cardsdom2  9970  aleph11  10064  alephiso  10078  fin23lem26  10304  compssiso  10353  isf34lem4  10356  isfin5-2  10370  fin1a2lem5  10383  brdom7disj  10510  brdom6disj  10511  fpwwe2lem7  10617  fpwwe2lem11  10621  fpwwe2lem12  10622  genpass  10989  ltasr  11080  axpre-lttri  11145  infm3  12169  creur  12207  eqreznegel  12953  rpneg  13045  ltxr  13135  icoshftf1o  13496  elfzm11  13619  elfzomelpfzo  13797  nn0ennn  14011  nnesq  14259  hashbclem  14485  hashf1lem1  14488  leiso  14492  fz1isolem  14494  pr2pwpr  14512  repsdf2  14811  dfrtrclrec2  15091  rexfiuz  15395  cau4  15404  ello1mpt2  15569  o1lo1  15584  fsumcom2  15821  incexc2  15888  fprodcom2  16034  dvdsflip  16370  bitsmod  16489  bitscmp  16491  smueqlem  16543  divgcdcoprm0  16718  hashdvds  16829  prmreclem2  16972  vdwapun  17029  vdwmc2  17034  imasaddfnlem  17577  comfeq  17757  oppcsect  17830  funcres2b  17949  funcpropd  17954  fullpropd  17974  fthpropd  17975  fthres2b  17984  fthres2c  17985  fullres2c  17993  ffthres2c  17994  fucsect  18027  fucinv  18028  setcsect  18141  pospropd  18376  tosso  18468  odulatb  18485  oduclatb  18558  odudlatb  18576  isipodrs  18588  mgmhmpropd  18751  issgrpv  18774  issgrpn0  18775  mndpropd  18812  mhmpropd  18845  issubm2  18857  efmnd1bas  18947  grppropd  19013  grpinvcnv  19068  qsxpid  19238  conjghm  19314  conjnmzb  19318  ghmpropd  19321  gapm  19371  symg1bas  19456  pmtrfrn  19523  cmnpropd  19856  ablpropd  19857  eqgabl  19899  gsumcom2  20040  dmdprd  20065  dprdw  20077  subgdmdprd  20101  pgpfac1lem2  20142  pgpfac1lem4  20145  rngpropd  20247  ringpropd  20367  crngpropd  20368  crngunit  20456  unitpropd  20495  isnirred  20498  nzrpropd  20618  issubrng  20646  subrngpropd  20667  resrhm2b  20701  subrgpropd  20707  rhmpropd  20708  rngcsect  20735  ringcsect  20769  isdomn3  20813  drngpropd  20873  fldpropd  20874  fiidomfld  20878  acsfn1p  20902  abvpropd  20938  lmodprop2d  21045  lsspropd  21138  lmhmpropd  21194  lbspropd  21220  lmhmlvec  21231  lvecprop2d  21290  lvecpropd  21291  df2idl2rng  21395  pzriprnglem10  21640  phlpropd  21805  assapropd  22021  psrbagconf1o  22079  mplmonmul  22187  ismhp3  22305  mat1dimbas  22629  tpspropd  23095  tgss2  23144  lmbr2  23416  ist1-2  23504  ist1-3  23506  subislly  23638  dissnlocfin  23686  iskgen3  23706  txcnmpt  23781  hausdiag  23802  hauseqlcld  23803  xkococnlem  23816  tgqtop  23869  txhmeo  23960  uffix2  24081  ufildr  24088  txflf  24163  tgphaus  24274  qustgplem  24278  qustgphaus  24280  xpsdsval  24538  blin  24578  blres  24588  xmeterval  24589  xmspropd  24630  mspropd  24631  setsms  24637  metequiv  24666  metustsym  24712  restmetu  24727  ngppropd  24794  xrtgioo  24964  metdsge  25007  icopnfcnv  25101  iccpnfcnv  25103  lmhmclm  25246  lmmbr  25417  equivcmet  25476  cmspropd  25508  iunmbl2  25716  ioombl1lem4  25720  mbfaddlem  25819  i1fmullem  25853  itg1mulc  25863  iblcnlem1  25947  iblrelem  25950  iblre  25953  iblcn  25958  limcun  26054  mvth  26151  ofmulrt  26440  resinf1o  26701  quad2  27004  1cubr  27007  dcubic  27011  wilthlem2  27233  dvdsflf1o  27351  dvdsflsumcom  27352  fsumvma  27377  vmasum  27380  logfac2  27381  logfaclbnd  27386  dchrelbas3  27402  lgsquadlem1  27544  lgsquadlem2  27545  eqcuts2  27979  mulsrid  28306  z12sge0  28676  readdscl  28692  elplng  29062  plngcplem  29067  ax5seg  29288  ushgredgedg  29579  ushgredgedgloop  29581  nbumgrvtx  29696  upgriswlk  29990  wspniunwspnon  30272  rusgrnumwwlkb0  30323  isclwwlknx  30387  clwwlknscsh  30413  clwwlknonel  30446  0trl  30473  0spth  30477  0clwlk  30481  0crct  30484  0cycl  30485  eupth2lem2  30570  eucrct2eupth  30596  fusgr2wsp2nb  30685  ocin  31648  chpsscon3  31855  chscllem2  31990  adjval  32242  pjimai  32528  mdsldmd1i  32683  elat2  32692  mdsymi  32763  sbceqbidf  32833  rmoxfrd  32839  rmounid  32841  disjxun0  32919  disjrdx  32936  eqrelrd2  32961  fmptcof2  33002  ofpreima  33010  funcnv5mpt  33012  ressupprn  33035  1stpreima  33052  2ndpreima  33053  fpwrelmapffslem  33077  cntrval2  33491  domnpropd  33600  idompropd  33601  subsdrg  33619  grplsm0l  33712  opprlidlabs  33767  ressply1mon1p  33858  psrmonmul  33940  algextdeglem6  34112  smatrcl  34186  locfinreflem  34230  zarcls  34264  zhmnrg  34355  qqhval2  34372  ismntop  34416  reprsuc  35002  reprdifc  35014  bnj919  35156  bnj956  35165  bnj976  35166  bnj1366  35217  bnj916  35321  satfvsucsuc  35857  satfdm  35861  dmopab3rexdif  35897  rexxfr3dALT  36131  sscoid  36403  dfrdg4  36443  altopthbg  36460  broutsideof3  36618  rmoeqbidv  36745  sbequbidv  36746  disjeq12dv  36747  ixpeq12dv  36748  cbvmodavw  36782  cbveudavw  36783  cbvrmodavw  36784  cbvreudavw  36785  cbvsbdavw  36786  cbvsbdavw2  36787  cbvabdavw  36788  cbvsbcdavw  36789  cbvsbcdavw2  36790  cbvdisjdavw  36800  cbvrmodavw2  36815  cbvreudavw2  36816  cbvdisjdavw2  36821  bj-nnfbi  37392  bj-cbvexdv  37455  bj-sbievw  37502  mobidvALT  37512  bj-axreprepsep  37732  bj-restuni  37759  bj-elid6  37834  cbveud  38038  cbvreud  38039  exrecfnlem  38045  wl-ifp-ncond2  38131  wl-ifpimpr  38132  wl-3xorbi123d  38141  wl-sb8eut  38253  wl-sb8eutv  38254  wl-sb8mot  38255  wl-sb8motv  38256  wl-clabtv  38261  wl-clabt  38262  wl-eujustlem1  38263  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem25  38316  ftc1anclem5  38368  istotbnd3  38442  sstotbnd  38446  heibor  38492  isass  38517  isidlc  38686  smprngopr  38723  brvvdif  38937  elecALTV  38940  eqrel2  38974  dmecd  38979  relcnveq2  38998  eldmxrncnvepres  39103  eldmxrncnvepres2  39104  extssr  39258  elrefrelsrel  39269  refreleq  39270  elcnvrefrelsrel  39285  elrelscnveq2  39298  elsymrelsrel  39310  symreleq  39311  eltrrelsrel  39334  trreleq  39335  eleqvrelsrel  39347  eqvreleq  39355  redundpim3  39383  erALTVeq1  39423  elfunsALTVfunALTV  39451  eldisjsdisj  39493  eldisjeq  39510  disjsuc  39528  parteq1  39546  parteq2  39547  islshpsm  39774  lcvexchlem1  39828  opcon1b  39992  isat3  40101  glbconN  40171  cdleme32fva  41231  cdlemg2cex  41385  dibelval3  41941  dib1dim  41959  doch11  42167  dochsordN  42168  mapdordlem1a  42428  mapd11  42433  mapdsord  42449  mapdcnv11N  42453  mapd0  42459  sn-iotalem  43012  ricfld  43318  fimgmcyc  43322  fsuppind  43342  mrefg2  43458  jm2.23  43743  wepwsolem  43789  dnwech  43795  islssfg2  43818  gicabl  43846  onsupmaxb  43986  onsupeqnmax  43994  orddif0suc  44015  oadif1lem  44126  oadif1  44127  fzunt  44201  fzuntd  44202  fzunt1d  44203  fzuntgd  44204  ifpbi2  44213  ifpbi3  44214  ifpbi1  44223  ifpbi12  44234  ifpbi13  44235  ontric3g  44268  pwinfig  44307  inintabd  44325  cnvcnvintabd  44346  cnvintabd  44349  intimag  44402  briunov2  44428  heeq12  44522  sbcheg  44525  uneqsn  44771  ntrneineine0lem  44829  ntrneineine1lem  44830  ntrneik2  44838  ntrneix2  44839  ntrneik13  44844  ntrneix13  44845  ralbidar  45174  rexbidar  45175  trsbc  45269  relpeq1  45673  relpeq2  45674  relpeq3  45675  relpeq4  45676  relpeq5  45677  n0abso  45705  modelaxreplem3  45709  iindif2f  45898  rnmptpr  45915  iccintsng  46259  xlimres  46555  fsetsniunop  47806  fsetsnprcnex  47812  fcoresf1ob  47830  f1cof1b  47834  f1ocof1ob  47838  dfateq12d  47883  aov0nbovbi  47952  fnotaovb  47955  ichbidv  48222  sprsymrelf  48264  prprsprreu  48288  prprreueq  48289  nprmmul1  48296  edgusgrclnbfin  48627  dfclnbgr6  48641  dfnbgr6  48642  isubgredg  48651  gpgnbgrvtx0  48859  gpgnbgrvtx1  48860  rngcsectALTV  49060  ringcsectALTV  49094  lindslinindsimp2lem5  49262  xpco2  49655  opndisj  49701  i0oii  49718  io1ii  49719  iscnrm3lem2  49733  uobffth  50016  uobeqw  50017  thincpropd  50240  termcpropd  50301  alsbid  50600