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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  pm5.32rd  589  orbi2d  929  orbi1d  930  ifpbi123d  1095  3orbi123d  1463  3anbi123d  1464  nanbi1  1531  nanbi2  1532  xorbi12d  1555  hadbi123d  1625  had0OLD  1636  cadbi123d  1643  nfbiit  1884  nfbidv  1955  sbequ  2120  nfbidf  2263  drex1v  2404  drnf1v  2405  drex1  2475  drnf1  2477  sb4b  2509  drsb1  2529  eujustALT  2602  eubi  2614  eleq1ab  2745  eqeq1d  2767  eqeq1dALT  2768  eqeq2d  2776  abbi  2830  eleq1w  2848  eleq2w  2849  eleq1d  2850  eleq2d  2851  eleq2dALT  2852  eqabdv  2898  nfceqdf  2923  drnfc1  2946  drnfc2  2947  neleq12d  3071  ralbidv2  3186  rexbidv2  3187  r19.21t  3261  r19.23t  3263  rexbida  3279  rexeq  3321  cbvraldva2  3342  raleqf  3347  ralcom2  3368  rmobidva  3384  reubidva  3385  rmobida  3394  reubida  3395  rmoeq1  3402  reueq1  3403  reueqbidv  3407  rmoeq1f  3408  reueq1f  3409  dfsbcq  3748  sbceqbid  3753  sbcbid  3800  sbcbi2  3804  eqsbc2  3809  sbcrext  3827  sbcabel  3832  ralss  4011  rexss  4012  psseq1  4045  psseq2  4046  ssconb  4096  uneq1  4115  difin2  4254  rcompleq  4258  reuun2  4278  sbcnel12g  4379  sbnfc2  4404  reldisj  4413  undif4  4427  disjssun  4428  pssdifcom1  4452  pssdifcom2  4453  sbcssg  4484  eltpg  4654  raltpg  4666  rextpg  4667  r19.12sn  4688  intmin4  4944  dfiun2g  4996  iindif1  5043  iindif2  5045  iinin2  5046  disjprg  5107  disjxun  5109  breq  5113  breq1  5114  breq2  5115  treq  5227  reusv2lem5  5375  rexxfrd  5382  rexxfr2d  5384  rexxfrd2  5386  rabxfrd  5390  opthg2  5463  oteqex2  5484  oteqex  5485  poeq1  5574  soeq1  5592  freq1  5630  weeq1  5650  weeq2  5651  opthprc  5727  wesn  5752  releq  5765  sbcrel  5769  eqrel  5772  eqrelrel  5785  xpiindi  5823  dmopab2rex  5909  dfres3  5985  brres  5987  resieq  5991  dmsnopg  6216  dfco2a  6249  dfpo2  6301  ordeq  6371  limeq  6376  ordunisssuc  6473  iotaeq  6508  sniota  6531  sbcfung  6564  imadif  6624  fneq1  6630  fneq2  6631  feq1  6687  feq2  6688  feq3  6689  sbcfng  6706  sbcfg  6707  f1eq1  6773  f1eq2  6774  f1eq3  6775  foeq1  6792  foeq2  6793  foeq3  6794  f1oeq1  6812  f1oeq2  6813  f1oeq3  6814  mpteqb  7013  rexrnmptw  7094  rexrnmpt  7096  dffo3  7101  dffo3f  7105  fmptco  7129  rexima  7243  dff13  7257  f1imaeq  7268  f1imapss  7269  cbvexfo  7297  f1eqcocnv  7308  fliftcnv  7318  isoeq1  7324  isoeq2  7325  isoeq3  7326  isoeq4  7327  isoeq5  7328  isomin  7344  isowe  7356  eqfunresadj  7369  nfriotadw  7384  mpoeq123  7491  rexrnmpo  7559  iunpw  7776  tfinds  7862  resf1extb  7937  fiun  7946  f1iun  7947  opiota  8062  xpord3pred  8154  ottpos  8238  dmtpos  8240  onoviun  8336  smoeq  8343  smoiso2  8362  tfr2b  8389  oarec  8553  oeeui  8594  nnacan  8620  nnmcan  8626  ereq1  8708  ereq2  8709  elecg  8745  ereldm  8754  ixpiin  8928  boxriin  8944  boxcutc  8945  omxpenlem  9073  enfiALT  9179  nnsdomo  9210  isfinite2  9265  ixpfi2  9314  elfi2  9381  fipwss  9396  ttrclse  9703  ennum  9949  cardsdom2  9990  aleph11  10084  alephiso  10098  fin23lem26  10324  compssiso  10373  isf34lem4  10376  isfin5-2  10390  fin1a2lem5  10403  brdom7disj  10531  brdom6disj  10532  fpwwe2lem7  10641  fpwwe2lem11  10645  fpwwe2lem12  10646  genpass  11013  ltasr  11104  axpre-lttri  11169  infm3  12193  creur  12231  eqreznegel  12978  rpneg  13070  ltxr  13160  icoshftf1o  13521  elfzm11  13644  elfzomelpfzo  13822  nn0ennn  14037  nnesq  14285  hashbclem  14511  hashf1lem1  14514  leiso  14518  fz1isolem  14520  pr2pwpr  14538  repsdf2  14843  dfrtrclrec2  15123  rexfiuz  15427  cau4  15436  ello1mpt2  15601  o1lo1  15616  fsumcom2  15852  incexc2  15919  fprodcom2  16065  dvdsflip  16401  bitsmod  16520  bitscmp  16522  smueqlem  16574  divgcdcoprm0  16749  hashdvds  16860  prmreclem2  17003  vdwapun  17060  vdwmc2  17065  imasaddfnlem  17608  comfeq  17788  oppcsect  17861  funcres2b  17980  funcpropd  17985  fullpropd  18005  fthpropd  18006  fthres2b  18015  fthres2c  18016  fullres2c  18024  ffthres2c  18025  fucsect  18058  fucinv  18059  setcsect  18172  pospropd  18407  tosso  18499  odulatb  18516  oduclatb  18589  odudlatb  18607  isipodrs  18619  mgmhmpropd  18792  issgrpv  18815  issgrpn0  18816  mndpropd  18856  mhmpropd  18891  issubm2  18903  efmnd1bas  18993  grppropd  19066  grpinvcnv  19121  qsxpid  19291  conjghm  19367  conjnmzb  19371  ghmpropd  19374  gapm  19424  symg1bas  19509  pmtrfrn  19576  cmnpropd  19909  ablpropd  19910  eqgabl  19952  gsumcom2  20093  dmdprd  20118  dprdw  20130  subgdmdprd  20154  pgpfac1lem2  20195  pgpfac1lem4  20198  rngpropd  20300  ringpropd  20421  crngpropd  20422  crngunit  20510  unitpropd  20549  isnirred  20552  nzrpropd  20672  issubrng  20700  subrngpropd  20721  resrhm2b  20755  subrgpropd  20761  rhmpropd  20762  rngcsect  20789  ringcsect  20823  isdomn3  20867  drngpropd  20927  fldpropd  20928  fiidomfld  20932  acsfn1p  20956  abvpropd  20992  lmodprop2d  21099  lsspropd  21192  lmhmpropd  21248  lbspropd  21274  lmhmlvec  21285  lvecprop2d  21344  lvecpropd  21345  df2idl2rng  21449  pzriprnglem10  21694  phlpropd  21859  assapropd  22075  psrbagconf1o  22133  mplmonmul  22241  ismhp3  22359  mat1dimbas  22683  tpspropd  23149  tgss2  23198  lmbr2  23470  ist1-2  23558  ist1-3  23560  subislly  23693  dissnlocfin  23741  iskgen3  23761  txcnmpt  23836  hausdiag  23857  hauseqlcld  23858  xkococnlem  23871  tgqtop  23924  txhmeo  24015  uffix2  24136  ufildr  24143  txflf  24218  tgphaus  24329  qustgplem  24333  qustgphaus  24335  xpsdsval  24593  blin  24633  blres  24643  xmeterval  24644  xmspropd  24685  mspropd  24686  setsms  24692  metequiv  24721  metustsym  24767  restmetu  24782  ngppropd  24849  xrtgioo  25019  metdsge  25062  icopnfcnv  25156  iccpnfcnv  25158  lmhmclm  25301  lmmbr  25472  equivcmet  25531  cmspropd  25563  iunmbl2  25771  ioombl1lem4  25775  mbfaddlem  25874  i1fmullem  25908  itg1mulc  25918  iblcnlem1  26002  iblrelem  26005  iblre  26008  iblcn  26013  limcun  26109  mvth  26206  ofmulrt  26495  resinf1o  26756  quad2  27059  1cubr  27062  dcubic  27066  wilthlem2  27288  dvdsflf1o  27406  dvdsflsumcom  27407  fsumvma  27432  vmasum  27435  logfac2  27436  logfaclbnd  27441  dchrelbas3  27457  lgsquadlem1  27599  lgsquadlem2  27600  eqcuts2  28034  mulsrid  28361  z12sge0  28731  readdscl  28747  elplng  29117  plngcplem  29122  ax5seg  29347  ushgredgedg  29641  ushgredgedgloop  29643  nbumgrvtx  29758  upgriswlk  30052  wspniunwspnon  30343  rusgrnumwwlkb0  30394  isclwwlknx  30458  clwwlknscsh  30484  clwwlknonel  30517  0trl  30544  0spth  30548  0clwlk  30552  0crct  30555  0cycl  30556  eupth2lem2  30645  eucrct2eupth  30671  fusgr2wsp2nb  30760  ocin  31723  chpsscon3  31930  chscllem2  32065  adjval  32317  pjimai  32603  mdsldmd1i  32758  elat2  32767  mdsymi  32838  sbceqbidf  32908  rmoxfrd  32914  rmounid  32916  disjxun0  32994  disjrdx  33011  eqrelrd2  33036  fmptcof2  33077  ofpreima  33085  funcnv5mpt  33087  ressupprn  33110  1stpreima  33127  2ndpreima  33128  fpwrelmapffslem  33151  cntrval2  33559  domnpropd  33668  idompropd  33669  subsdrg  33687  grplsm0l  33780  opprlidlabs  33835  ressply1mon1p  33926  psrmonmul  34008  algextdeglem6  34180  smatrcl  34254  locfinreflem  34298  zarcls  34332  zhmnrg  34423  qqhval2  34440  ismntop  34484  reprsuc  35071  reprdifc  35083  bnj919  35225  bnj956  35234  bnj976  35235  bnj1366  35286  bnj916  35390  satfvsucsuc  35898  satfdm  35902  dmopab3rexdif  35938  rexxfr3dALT  36172  sscoid  36444  dfrdg4  36484  altopthbg  36501  broutsideof3  36659  rmoeqbidv  36786  sbequbidv  36787  disjeq12dv  36788  ixpeq12dv  36789  cbvmodavw  36823  cbveudavw  36824  cbvrmodavw  36825  cbvreudavw  36826  cbvsbdavw  36827  cbvsbdavw2  36828  cbvabdavw  36829  cbvsbcdavw  36830  cbvsbcdavw2  36831  cbvdisjdavw  36841  cbvrmodavw2  36856  cbvreudavw2  36857  cbvdisjdavw2  36862  bj-nnfbi  37433  bj-cbvexdv  37496  bj-sbievw  37543  mobidvALT  37553  bj-axreprepsep  37773  bj-restuni  37800  bj-elid6  37875  cbveud  38079  cbvreud  38080  exrecfnlem  38086  wl-ifp-ncond2  38172  wl-ifpimpr  38173  wl-3xorbi123d  38182  wl-sb8eut  38294  wl-sb8eutv  38295  wl-sb8mot  38296  wl-sb8motv  38297  wl-clabtv  38302  wl-clabt  38303  wl-eujustlem1  38304  poimirlem17  38349  poimirlem19  38351  poimirlem20  38352  poimirlem25  38357  ftc1anclem5  38409  istotbnd3  38484  sstotbnd  38488  heibor  38534  isass  38559  isidlc  38728  smprngopr  38765  brvvdif  38979  elecALTV  38982  eqrel2  39016  dmecd  39021  relcnveq2  39040  eldmxrncnvepres  39145  eldmxrncnvepres2  39146  extssr  39300  elrefrelsrel  39311  refreleq  39312  elcnvrefrelsrel  39327  elrelscnveq2  39340  elsymrelsrel  39352  symreleq  39353  eltrrelsrel  39376  trreleq  39377  eleqvrelsrel  39389  eqvreleq  39397  redundpim3  39425  erALTVeq1  39465  elfunsALTVfunALTV  39493  eldisjsdisj  39535  eldisjeq  39552  disjsuc  39570  parteq1  39588  parteq2  39589  islshpsm  39816  lcvexchlem1  39870  opcon1b  40034  isat3  40143  glbconN  40213  cdleme32fva  41273  cdlemg2cex  41427  dibelval3  41983  dib1dim  42001  doch11  42209  dochsordN  42210  mapdordlem1a  42470  mapd11  42475  mapdsord  42491  mapdcnv11N  42495  mapd0  42501  sn-iotalem  43054  ricfld  43375  fimgmcyc  43379  fsuppind  43399  mrefg2  43515  jm2.23  43800  wepwsolem  43846  dnwech  43852  islssfg2  43875  gicabl  43903  onsupmaxb  44043  onsupeqnmax  44051  orddif0suc  44072  oadif1lem  44183  oadif1  44184  fzunt  44258  fzuntd  44259  fzunt1d  44260  fzuntgd  44261  ifpbi2  44270  ifpbi3  44271  ifpbi1  44280  ifpbi12  44291  ifpbi13  44292  ontric3g  44325  pwinfig  44364  inintabd  44382  cnvcnvintabd  44403  cnvintabd  44406  intimag  44459  briunov2  44485  heeq12  44579  sbcheg  44582  uneqsn  44828  ntrneineine0lem  44886  ntrneineine1lem  44887  ntrneik2  44895  ntrneix2  44896  ntrneik13  44901  ntrneix13  44902  ralbidar  45231  rexbidar  45232  trsbc  45326  relpeq1  45730  relpeq2  45731  relpeq3  45732  relpeq4  45733  relpeq5  45734  n0abso  45762  modelaxreplem3  45766  iindif2f  45955  rnmptpr  45972  iccintsng  46316  xlimres  46612  fsetsniunop  47863  fsetsnprcnex  47869  fcoresf1ob  47887  f1cof1b  47891  f1ocof1ob  47895  dfateq12d  47940  aov0nbovbi  48009  fnotaovb  48012  ichbidv  48279  sprsymrelf  48321  prprsprreu  48345  prprreueq  48346  nprmmul1  48353  edgusgrclnbfin  48684  dfclnbgr6  48698  dfnbgr6  48699  isubgredg  48708  gpgnbgrvtx0  48916  gpgnbgrvtx1  48917  rngcsectALTV  49116  ringcsectALTV  49150  lindslinindsimp2lem5  49318  xpco2  49711  opndisj  49757  i0oii  49774  io1ii  49775  iscnrm3lem2  49789  uobffth  50072  uobeqw  50073  thincpropd  50296  termcpropd  50357  alsbid  50656