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  3229  r19.23t  3231  rexbida  3247  rexeq  3292  raleqbidvvOLD  3305  cbvraldva2  3318  cbvrexdva2OLD  3320  raleqf  3326  rexeqfOLD  3328  ralcom2  3348  rmobidva  3366  reubidva  3367  rmobida  3376  reubida  3377  rmoeq1  3384  reueq1  3385  rmoeq1OLD  3386  reueq1OLD  3387  reueqbidv  3391  rmoeq1f  3392  reueq1f  3393  dfsbcq  3752  sbceqbid  3757  sbcbid  3805  sbcbi2  3809  eqsbc2  3814  sbcrext  3833  sbcabel  3838  ralss  4018  rexss  4019  psseq1  4049  psseq2  4050  ssconb  4101  uneq1  4120  difin2  4260  rcompleq  4264  reuun2  4284  sbcnel12g  4373  sbnfc2  4398  reldisj  4412  undif4  4426  disjssun  4427  pssdifcom1  4449  pssdifcom2  4450  sbcssg  4479  eltpg  4646  raltpg  4658  rextpg  4659  r19.12sn  4680  intmin4  4937  dfiun2g  4990  iindif1  5034  iindif2  5036  iinin2  5037  disjprg  5098  disjxun  5100  breq  5104  breq1  5105  breq2  5106  treq  5217  reusv2lem5  5352  rexxfrd  5359  rexxfr2d  5361  rexxfrd2  5363  rabxfrd  5367  opthg2  5434  oteqex2  5454  oteqex  5455  poeq1  5542  soeq1  5560  freq1  5598  weeq1  5618  weeq2  5619  opthprc  5695  wesn  5720  releq  5731  sbcrel  5735  eqrel  5738  eqrelrel  5751  xpiindi  5789  dmopab2rex  5871  dfres3  5944  brres  5946  resieq  5950  dmsnopg  6174  dfco2a  6207  dfpo2  6257  ordeq  6327  limeq  6332  ordunisssuc  6428  iotaeq  6464  sniota  6490  sbcfung  6524  imadif  6584  fneq1  6591  fneq2  6592  feq1  6648  feq2  6649  feq3  6650  sbcfng  6667  sbcfg  6668  f1eq1  6733  f1eq2  6734  f1eq3  6735  foeq1  6750  foeq2  6751  foeq3  6752  f1oeq1  6770  f1oeq2  6771  f1oeq3  6772  mpteqb  6969  rexrnmptw  7049  rexrnmpt  7051  dffo3  7056  dffo3f  7060  fmptco  7083  rexima  7194  dff13  7211  f1imaeq  7222  f1imapss  7223  cbvexfo  7247  f1eqcocnv  7258  fliftcnv  7268  isoeq1  7274  isoeq2  7275  isoeq3  7276  isoeq4  7277  isoeq5  7278  isomin  7294  isowe  7306  eqfunresadj  7317  imaeqsalvOLD  7321  nfriotadw  7334  mpoeq123  7441  rexrnmpo  7509  iunpw  7727  tfinds  7816  resf1extb  7890  fiun  7901  f1iun  7902  opiota  8017  xpord3pred  8108  ottpos  8192  dmtpos  8194  onoviun  8289  smoeq  8296  smoiso2  8315  tfr2b  8341  oarec  8503  oeeui  8543  nnacan  8569  nnmcan  8575  ereq1  8655  ereq2  8656  elecg  8692  ereldm  8701  ixpiin  8874  boxriin  8890  boxcutc  8891  omxpenlem  9019  enfiALT  9129  nnsdomo  9159  isfinite2  9221  ixpfi2  9277  elfi2  9341  fipwss  9356  ttrclse  9656  ennum  9876  cardsdom2  9917  aleph11  10013  alephiso  10027  fin23lem26  10254  compssiso  10303  isf34lem4  10306  isfin5-2  10320  fin1a2lem5  10333  brdom7disj  10460  brdom6disj  10461  fpwwe2lem7  10566  fpwwe2lem11  10570  fpwwe2lem12  10571  genpass  10938  ltasr  11029  axpre-lttri  11094  infm3  12118  creur  12156  eqreznegel  12869  rpneg  12961  ltxr  13051  icoshftf1o  13411  elfzm11  13532  elfzomelpfzo  13708  nn0ennn  13920  nnesq  14168  hashbclem  14393  hashf1lem1  14396  leiso  14400  fz1isolem  14402  pr2pwpr  14420  repsdf2  14719  dfrtrclrec2  15000  rexfiuz  15290  cau4  15299  ello1mpt2  15464  o1lo1  15479  fsumcom2  15716  incexc2  15780  fprodcom2  15926  dvdsflip  16263  bitsmod  16382  bitscmp  16384  smueqlem  16436  divgcdcoprm0  16611  hashdvds  16721  prmreclem2  16864  vdwapun  16921  vdwmc2  16926  imasaddfnlem  17467  comfeq  17647  oppcsect  17720  funcres2b  17839  funcpropd  17844  fullpropd  17864  fthpropd  17865  fthres2b  17874  fthres2c  17875  fullres2c  17883  ffthres2c  17884  fucsect  17917  fucinv  17918  setcsect  18031  pospropd  18266  tosso  18358  odulatb  18375  oduclatb  18448  odudlatb  18466  isipodrs  18478  mgmhmpropd  18607  issgrpv  18630  issgrpn0  18631  mndpropd  18668  mhmpropd  18701  issubm2  18713  efmnd1bas  18802  grppropd  18865  grpinvcnv  18920  conjghm  19163  conjnmzb  19167  ghmpropd  19170  gapm  19220  symg1bas  19305  pmtrfrn  19372  cmnpropd  19705  ablpropd  19706  eqgabl  19748  gsumcom2  19889  dmdprd  19914  dprdw  19926  subgdmdprd  19950  pgpfac1lem2  19991  pgpfac1lem4  19994  rngpropd  20094  ringpropd  20208  crngpropd  20209  crngunit  20298  unitpropd  20337  isnirred  20340  nzrpropd  20440  issubrng  20467  subrngpropd  20488  resrhm2b  20522  subrgpropd  20528  rhmpropd  20529  rngcsect  20556  ringcsect  20590  isdomn3  20635  drngpropd  20689  fldpropd  20690  fiidomfld  20694  acsfn1p  20719  abvpropd  20755  lmodprop2d  20862  lsspropd  20956  lmhmpropd  21012  lbspropd  21038  lmhmlvec  21049  lvecprop2d  21108  lvecpropd  21109  df2idl2rng  21198  pzriprnglem10  21432  phlpropd  21597  assapropd  21814  psrbagconf1o  21871  mplmonmul  21976  ismhp3  22062  mat1dimbas  22392  tpspropd  22858  tgss2  22907  lmbr2  23179  ist1-2  23267  ist1-3  23269  subislly  23401  dissnlocfin  23449  iskgen3  23469  txcnmpt  23544  hausdiag  23565  hauseqlcld  23566  xkococnlem  23579  tgqtop  23632  txhmeo  23723  uffix2  23844  ufildr  23851  txflf  23926  tgphaus  24037  qustgplem  24041  qustgphaus  24043  xpsdsval  24302  blin  24342  blres  24352  xmeterval  24353  xmspropd  24394  mspropd  24395  setsms  24401  metequiv  24430  metustsym  24476  restmetu  24491  ngppropd  24558  xrtgioo  24728  metdsge  24771  icopnfcnv  24873  iccpnfcnv  24875  lmhmclm  25020  lmmbr  25191  equivcmet  25250  cmspropd  25282  iunmbl2  25491  ioombl1lem4  25495  mbfaddlem  25594  i1fmullem  25628  itg1mulc  25638  iblcnlem1  25722  iblrelem  25725  iblre  25728  iblcn  25733  limcun  25829  mvth  25930  ofmulrt  26222  resinf1o  26478  quad2  26782  1cubr  26785  dcubic  26789  wilthlem2  27012  dvdsflf1o  27130  dvdsflsumcom  27131  fsumvma  27157  vmasum  27160  logfac2  27161  logfaclbnd  27166  dchrelbas3  27182  lgsquadlem1  27324  lgsquadlem2  27325  eqscut2  27752  mulsrid  28056  zs12ge0  28395  readdscl  28403  ax5seg  28918  ushgredgedg  29209  ushgredgedgloop  29211  nbumgrvtx  29326  upgriswlk  29621  wspniunwspnon  29903  rusgrnumwwlkb0  29951  isclwwlknx  30015  clwwlknscsh  30041  clwwlknonel  30074  0trl  30101  0spth  30105  0clwlk  30109  0crct  30112  0cycl  30113  eupth2lem2  30198  eucrct2eupth  30224  fusgr2wsp2nb  30313  ocin  31275  chpsscon3  31482  chscllem2  31617  adjval  31869  pjimai  32155  mdsldmd1i  32310  elat2  32319  mdsymi  32390  sbceqbidf  32466  rmoxfrd  32472  rmounid  32474  disjxun0  32553  disjrdx  32570  eqrelrd2  32594  fmptcof2  32631  ofpreima  32639  funcnv5mpt  32642  ressupprn  32663  1stpreima  32680  2ndpreima  32681  fpwrelmapffslem  32705  cntrval2  33143  domnpropd  33243  idompropd  33244  subsdrg  33264  qsxpid  33326  grplsm0l  33367  opprlidlabs  33449  ressply1mon1p  33530  algextdeglem6  33705  smatrcl  33779  locfinreflem  33823  zarcls  33857  zhmnrg  33948  qqhval2  33965  ismntop  34009  reprsuc  34599  reprdifc  34611  bnj919  34750  bnj956  34759  bnj976  34760  bnj1366  34812  bnj916  34916  satfvsucsuc  35345  satfdm  35349  dmopab3rexdif  35385  rexxfr3dALT  35619  sscoid  35894  dfrdg4  35932  altopthbg  35949  broutsideof3  36107  rmoeqbidv  36194  sbequbidv  36195  disjeq12dv  36196  ixpeq12dv  36197  cbvmodavw  36231  cbveudavw  36232  cbvrmodavw  36233  cbvreudavw  36234  cbvsbdavw  36235  cbvsbdavw2  36236  cbvabdavw  36237  cbvsbcdavw  36238  cbvsbcdavw2  36239  cbvdisjdavw  36249  cbvrmodavw2  36264  cbvreudavw2  36265  cbvdisjdavw2  36270  bj-nnfbi  36706  bj-cbvexdv  36781  bj-sbievw  36828  mobidvALT  36838  bj-restuni  37078  bj-elid6  37151  cbveud  37353  cbvreud  37354  exrecfnlem  37360  wl-ifp-ncond2  37446  wl-ifpimpr  37447  wl-3xorbi123d  37456  wl-sb8eut  37559  wl-sb8eutv  37560  wl-sb8mot  37561  wl-sb8motv  37562  wl-clabtv  37578  wl-clabt  37579  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem25  37632  ftc1anclem5  37684  istotbnd3  37758  sstotbnd  37762  heibor  37808  isass  37833  isidlc  38002  smprngopr  38039  brvvdif  38245  elecALTV  38248  eqrel2  38280  dmecd  38285  relcnveq2  38304  eldmxrncnvepres  38389  eldmxrncnvepres2  38390  elrelscnveq2  38477  extssr  38493  elrefrelsrel  38504  refreleq  38505  elcnvrefrelsrel  38520  elsymrelsrel  38541  symreleq  38542  eltrrelsrel  38565  trreleq  38566  eleqvrelsrel  38578  eqvreleq  38586  redundpim3  38614  erALTVeq1  38654  elfunsALTVfunALTV  38682  eldisjsdisj  38712  eldisjeq  38726  disjsuc  38744  parteq1  38759  parteq2  38760  islshpsm  38966  lcvexchlem1  39020  opcon1b  39184  isat3  39293  glbconN  39363  glbconNOLD  39364  cdleme32fva  40424  cdlemg2cex  40578  dibelval3  41134  dib1dim  41152  doch11  41360  dochsordN  41361  mapdordlem1a  41621  mapd11  41626  mapdsord  41642  mapdcnv11N  41646  mapd0  41652  sn-iotalem  42202  ricfld  42511  fimgmcyc  42515  fsuppind  42571  mrefg2  42688  jm2.23  42978  wepwsolem  43024  dnwech  43030  islssfg2  43053  gicabl  43081  onsupmaxb  43221  onsupeqnmax  43229  orddif0suc  43250  oadif1lem  43361  oadif1  43362  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  ifpbi2  43449  ifpbi3  43450  ifpbi1  43459  ifpbi12  43470  ifpbi13  43471  ontric3g  43504  pwinfig  43543  inintabd  43561  cnvcnvintabd  43582  cnvintabd  43585  intimag  43638  briunov2  43664  heeq12  43758  sbcheg  43761  uneqsn  44007  ntrneineine0lem  44065  ntrneineine1lem  44066  ntrneik2  44074  ntrneix2  44075  ntrneik13  44080  ntrneix13  44081  ralbidar  44427  rexbidar  44428  trsbc  44523  relpeq1  44927  relpeq2  44928  relpeq3  44929  relpeq4  44930  relpeq5  44931  n0abso  44959  modelaxreplem3  44963  iindif2f  45147  rnmptpr  45164  iccintsng  45514  xlimres  45812  fsetsniunop  47043  fsetsnprcnex  47049  fcoresf1ob  47067  f1cof1b  47071  f1ocof1ob  47075  dfateq12d  47120  aov0nbovbi  47189  fnotaovb  47192  ichbidv  47447  sprsymrelf  47489  prprsprreu  47513  prprreueq  47514  edgusgrclnbfin  47835  dfclnbgr6  47849  dfnbgr6  47850  isubgredg  47859  gpgnbgrvtx0  48058  gpgnbgrvtx1  48059  rngcsectALTV  48256  ringcsectALTV  48290  lindslinindsimp2lem5  48444  xpco2  48838  opndisj  48884  i0oii  48901  io1ii  48902  iscnrm3lem2  48916  uobffth  49200  uobeqw  49201  thincpropd  49424  termcpropd  49485