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  1502  nanbi2  1503  xorbi12d  1526  hadbi123d  1596  had0  1605  cadbi123d  1611  nfbiit  1852  nfbidv  1923  sbequ  2086  nfbidf  2227  drex1v  2370  drnf1v  2371  drex1  2441  drnf1  2443  sb4b  2475  drsb1  2495  eujustALT  2567  eubi  2579  eleq1ab  2711  eqeq1d  2733  eqeq1dALT  2734  eqeq2d  2742  abbi  2796  eleq1w  2814  eleq2w  2815  eleq1d  2816  eleq2d  2817  eleq2dALT  2818  eqabdv  2864  nfceqdf  2890  drnfc1  2914  drnfc2  2915  neleq12d  3037  ralbidv2  3151  rexbidv2  3152  r19.21t  3226  r19.23t  3228  rexbida  3244  rexeq  3288  raleqbidvvOLD  3301  cbvraldva2  3314  raleqf  3321  rexeqfOLD  3323  ralcom2  3343  rmobidva  3359  reubidva  3360  rmobida  3369  reubida  3370  rmoeq1  3377  reueq1  3378  rmoeq1OLD  3379  reueq1OLD  3380  reueqbidv  3384  rmoeq1f  3385  reueq1f  3386  dfsbcq  3738  sbceqbid  3743  sbcbid  3791  sbcbi2  3795  eqsbc2  3800  sbcrext  3819  sbcabel  3824  ralss  4004  rexss  4005  psseq1  4037  psseq2  4038  ssconb  4089  uneq1  4108  difin2  4248  rcompleq  4252  reuun2  4272  sbcnel12g  4361  sbnfc2  4386  reldisj  4400  undif4  4414  disjssun  4415  pssdifcom1  4437  pssdifcom2  4438  sbcssg  4467  eltpg  4636  raltpg  4648  rextpg  4649  r19.12sn  4670  intmin4  4925  dfiun2g  4978  iindif1  5021  iindif2  5023  iinin2  5024  disjprg  5085  disjxun  5087  breq  5091  breq1  5092  breq2  5093  treq  5203  reusv2lem5  5338  rexxfrd  5345  rexxfr2d  5347  rexxfrd2  5349  rabxfrd  5353  opthg2  5417  oteqex2  5437  oteqex  5438  poeq1  5525  soeq1  5543  freq1  5581  weeq1  5601  weeq2  5602  opthprc  5678  wesn  5703  releq  5716  sbcrel  5720  eqrel  5723  eqrelrel  5736  xpiindi  5774  dmopab2rex  5856  dfres3  5932  brres  5934  resieq  5938  dmsnopg  6160  dfco2a  6193  dfpo2  6243  ordeq  6313  limeq  6318  ordunisssuc  6414  iotaeq  6449  sniota  6472  sbcfung  6505  imadif  6565  fneq1  6572  fneq2  6573  feq1  6629  feq2  6630  feq3  6631  sbcfng  6648  sbcfg  6649  f1eq1  6714  f1eq2  6715  f1eq3  6716  foeq1  6731  foeq2  6732  foeq3  6733  f1oeq1  6751  f1oeq2  6752  f1oeq3  6753  mpteqb  6948  rexrnmptw  7028  rexrnmpt  7030  dffo3  7035  dffo3f  7039  fmptco  7062  rexima  7172  dff13  7188  f1imaeq  7199  f1imapss  7200  cbvexfo  7224  f1eqcocnv  7235  fliftcnv  7245  isoeq1  7251  isoeq2  7252  isoeq3  7253  isoeq4  7254  isoeq5  7255  isomin  7271  isowe  7283  eqfunresadj  7294  imaeqsalvOLD  7298  nfriotadw  7311  mpoeq123  7418  rexrnmpo  7486  iunpw  7704  tfinds  7790  resf1extb  7864  fiun  7875  f1iun  7876  opiota  7991  xpord3pred  8082  ottpos  8166  dmtpos  8168  onoviun  8263  smoeq  8270  smoiso2  8289  tfr2b  8315  oarec  8477  oeeui  8517  nnacan  8543  nnmcan  8549  ereq1  8629  ereq2  8630  elecg  8666  ereldm  8675  ixpiin  8848  boxriin  8864  boxcutc  8865  omxpenlem  8991  enfiALT  9097  nnsdomo  9127  isfinite2  9182  ixpfi2  9234  elfi2  9298  fipwss  9313  ttrclse  9617  ennum  9840  cardsdom2  9881  aleph11  9975  alephiso  9989  fin23lem26  10216  compssiso  10265  isf34lem4  10268  isfin5-2  10282  fin1a2lem5  10295  brdom7disj  10422  brdom6disj  10423  fpwwe2lem7  10528  fpwwe2lem11  10532  fpwwe2lem12  10533  genpass  10900  ltasr  10991  axpre-lttri  11056  infm3  12081  creur  12119  eqreznegel  12832  rpneg  12924  ltxr  13014  icoshftf1o  13374  elfzm11  13495  elfzomelpfzo  13672  nn0ennn  13886  nnesq  14134  hashbclem  14359  hashf1lem1  14362  leiso  14366  fz1isolem  14368  pr2pwpr  14386  repsdf2  14685  dfrtrclrec2  14965  rexfiuz  15255  cau4  15264  ello1mpt2  15429  o1lo1  15444  fsumcom2  15681  incexc2  15745  fprodcom2  15891  dvdsflip  16228  bitsmod  16347  bitscmp  16349  smueqlem  16401  divgcdcoprm0  16576  hashdvds  16686  prmreclem2  16829  vdwapun  16886  vdwmc2  16891  imasaddfnlem  17432  comfeq  17612  oppcsect  17685  funcres2b  17804  funcpropd  17809  fullpropd  17829  fthpropd  17830  fthres2b  17839  fthres2c  17840  fullres2c  17848  ffthres2c  17849  fucsect  17882  fucinv  17883  setcsect  17996  pospropd  18231  tosso  18323  odulatb  18340  oduclatb  18413  odudlatb  18431  isipodrs  18443  mgmhmpropd  18606  issgrpv  18629  issgrpn0  18630  mndpropd  18667  mhmpropd  18700  issubm2  18712  efmnd1bas  18801  grppropd  18864  grpinvcnv  18919  conjghm  19161  conjnmzb  19165  ghmpropd  19168  gapm  19218  symg1bas  19303  pmtrfrn  19370  cmnpropd  19703  ablpropd  19704  eqgabl  19746  gsumcom2  19887  dmdprd  19912  dprdw  19924  subgdmdprd  19948  pgpfac1lem2  19989  pgpfac1lem4  19992  rngpropd  20092  ringpropd  20206  crngpropd  20207  crngunit  20296  unitpropd  20335  isnirred  20338  nzrpropd  20435  issubrng  20462  subrngpropd  20483  resrhm2b  20517  subrgpropd  20523  rhmpropd  20524  rngcsect  20551  ringcsect  20585  isdomn3  20630  drngpropd  20684  fldpropd  20685  fiidomfld  20689  acsfn1p  20714  abvpropd  20750  lmodprop2d  20857  lsspropd  20951  lmhmpropd  21007  lbspropd  21033  lmhmlvec  21044  lvecprop2d  21103  lvecpropd  21104  df2idl2rng  21193  pzriprnglem10  21427  phlpropd  21592  assapropd  21809  psrbagconf1o  21866  mplmonmul  21971  ismhp3  22057  mat1dimbas  22387  tpspropd  22853  tgss2  22902  lmbr2  23174  ist1-2  23262  ist1-3  23264  subislly  23396  dissnlocfin  23444  iskgen3  23464  txcnmpt  23539  hausdiag  23560  hauseqlcld  23561  xkococnlem  23574  tgqtop  23627  txhmeo  23718  uffix2  23839  ufildr  23846  txflf  23921  tgphaus  24032  qustgplem  24036  qustgphaus  24038  xpsdsval  24296  blin  24336  blres  24346  xmeterval  24347  xmspropd  24388  mspropd  24389  setsms  24395  metequiv  24424  metustsym  24470  restmetu  24485  ngppropd  24552  xrtgioo  24722  metdsge  24765  icopnfcnv  24867  iccpnfcnv  24869  lmhmclm  25014  lmmbr  25185  equivcmet  25244  cmspropd  25276  iunmbl2  25485  ioombl1lem4  25489  mbfaddlem  25588  i1fmullem  25622  itg1mulc  25632  iblcnlem1  25716  iblrelem  25719  iblre  25722  iblcn  25727  limcun  25823  mvth  25924  ofmulrt  26216  resinf1o  26472  quad2  26776  1cubr  26779  dcubic  26783  wilthlem2  27006  dvdsflf1o  27124  dvdsflsumcom  27125  fsumvma  27151  vmasum  27154  logfac2  27155  logfaclbnd  27160  dchrelbas3  27176  lgsquadlem1  27318  lgsquadlem2  27319  eqscut2  27747  mulsrid  28052  zs12ge0  28393  readdscl  28401  ax5seg  28916  ushgredgedg  29207  ushgredgedgloop  29209  nbumgrvtx  29324  upgriswlk  29619  wspniunwspnon  29901  rusgrnumwwlkb0  29952  isclwwlknx  30016  clwwlknscsh  30042  clwwlknonel  30075  0trl  30102  0spth  30106  0clwlk  30110  0crct  30113  0cycl  30114  eupth2lem2  30199  eucrct2eupth  30225  fusgr2wsp2nb  30314  ocin  31276  chpsscon3  31483  chscllem2  31618  adjval  31870  pjimai  32156  mdsldmd1i  32311  elat2  32320  mdsymi  32391  sbceqbidf  32466  rmoxfrd  32472  rmounid  32474  disjxun0  32554  disjrdx  32571  eqrelrd2  32599  fmptcof2  32639  ofpreima  32647  funcnv5mpt  32650  ressupprn  32671  1stpreima  32688  2ndpreima  32689  fpwrelmapffslem  32715  cntrval2  33140  domnpropd  33243  idompropd  33244  subsdrg  33264  qsxpid  33327  grplsm0l  33368  opprlidlabs  33450  ressply1mon1p  33531  algextdeglem6  33735  smatrcl  33809  locfinreflem  33853  zarcls  33887  zhmnrg  33978  qqhval2  33995  ismntop  34039  reprsuc  34628  reprdifc  34640  bnj919  34779  bnj956  34788  bnj976  34789  bnj1366  34841  bnj916  34945  satfvsucsuc  35409  satfdm  35413  dmopab3rexdif  35449  rexxfr3dALT  35683  sscoid  35955  dfrdg4  35995  altopthbg  36012  broutsideof3  36170  rmoeqbidv  36257  sbequbidv  36258  disjeq12dv  36259  ixpeq12dv  36260  cbvmodavw  36294  cbveudavw  36295  cbvrmodavw  36296  cbvreudavw  36297  cbvsbdavw  36298  cbvsbdavw2  36299  cbvabdavw  36300  cbvsbcdavw  36301  cbvsbcdavw2  36302  cbvdisjdavw  36312  cbvrmodavw2  36327  cbvreudavw2  36328  cbvdisjdavw2  36333  bj-nnfbi  36769  bj-cbvexdv  36844  bj-sbievw  36891  mobidvALT  36901  bj-restuni  37141  bj-elid6  37214  cbveud  37416  cbvreud  37417  exrecfnlem  37423  wl-ifp-ncond2  37509  wl-ifpimpr  37510  wl-3xorbi123d  37519  wl-sb8eut  37622  wl-sb8eutv  37623  wl-sb8mot  37624  wl-sb8motv  37625  wl-clabtv  37641  wl-clabt  37642  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem25  37695  ftc1anclem5  37747  istotbnd3  37821  sstotbnd  37825  heibor  37871  isass  37896  isidlc  38065  smprngopr  38102  brvvdif  38310  elecALTV  38313  eqrel2  38347  dmecd  38352  relcnveq2  38371  eldmxrncnvepres  38468  eldmxrncnvepres2  38469  extssr  38611  elrefrelsrel  38622  refreleq  38623  elcnvrefrelsrel  38638  elrelscnveq2  38651  elsymrelsrel  38663  symreleq  38664  eltrrelsrel  38687  trreleq  38688  eleqvrelsrel  38700  eqvreleq  38708  redundpim3  38736  erALTVeq1  38777  elfunsALTVfunALTV  38805  eldisjsdisj  38835  eldisjeq  38849  disjsuc  38867  parteq1  38882  parteq2  38883  islshpsm  39089  lcvexchlem1  39143  opcon1b  39307  isat3  39416  glbconN  39486  cdleme32fva  40546  cdlemg2cex  40700  dibelval3  41256  dib1dim  41274  doch11  41482  dochsordN  41483  mapdordlem1a  41743  mapd11  41748  mapdsord  41764  mapdcnv11N  41768  mapd0  41774  sn-iotalem  42324  ricfld  42633  fimgmcyc  42637  fsuppind  42693  mrefg2  42810  jm2.23  43099  wepwsolem  43145  dnwech  43151  islssfg2  43174  gicabl  43202  onsupmaxb  43342  onsupeqnmax  43350  orddif0suc  43371  oadif1lem  43482  oadif1  43483  fzunt  43558  fzuntd  43559  fzunt1d  43560  fzuntgd  43561  ifpbi2  43570  ifpbi3  43571  ifpbi1  43580  ifpbi12  43591  ifpbi13  43592  ontric3g  43625  pwinfig  43664  inintabd  43682  cnvcnvintabd  43703  cnvintabd  43706  intimag  43759  briunov2  43785  heeq12  43879  sbcheg  43882  uneqsn  44128  ntrneineine0lem  44186  ntrneineine1lem  44187  ntrneik2  44195  ntrneix2  44196  ntrneik13  44201  ntrneix13  44202  ralbidar  44547  rexbidar  44548  trsbc  44643  relpeq1  45047  relpeq2  45048  relpeq3  45049  relpeq4  45050  relpeq5  45051  n0abso  45079  modelaxreplem3  45083  iindif2f  45267  rnmptpr  45284  iccintsng  45633  xlimres  45929  fsetsniunop  47159  fsetsnprcnex  47165  fcoresf1ob  47183  f1cof1b  47187  f1ocof1ob  47191  dfateq12d  47236  aov0nbovbi  47305  fnotaovb  47308  ichbidv  47563  sprsymrelf  47605  prprsprreu  47629  prprreueq  47630  edgusgrclnbfin  47952  dfclnbgr6  47966  dfnbgr6  47967  isubgredg  47976  gpgnbgrvtx0  48184  gpgnbgrvtx1  48185  rngcsectALTV  48385  ringcsectALTV  48419  lindslinindsimp2lem5  48573  xpco2  48967  opndisj  49013  i0oii  49030  io1ii  49031  iscnrm3lem2  49045  uobffth  49329  uobeqw  49330  thincpropd  49553  termcpropd  49614