MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4g Structured version   Visualization version   GIF version

Theorem 3bitr4g 302
Description: More general version of 3bitr4i 291. 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
StepHypRef Expression
1 3bitr4g.2 . . 3 (𝜃𝜓)
2 3bitr4g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bb 271 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 277 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  bibi1d  332  pm5.32rd  670  orbi2d  734  orbi1d  735  ifpbi123d  1021  3orbi123d  1390  3anbi123d  1391  nanbi1  1447  nanbi2  1448  xorbi12d  1470  hadbi123d  1525  had0  1534  cadbi123d  1540  19.23t  2066  nfbidf  2079  nfbidfOLD  2189  19.23tOLD  2206  cbvexd  2266  drex1  2315  drnf1  2317  drsb1  2365  eujustALT  2461  eubid  2476  mobid  2477  eqeq1d  2612  eqeq1dALT  2613  eqeq2d  2620  eleq1d  2672  eleq2d  2673  eleq2dOLD  2674  eleq2dALT  2675  nfceqdf  2747  drnfc1  2768  drnfc2  2769  neleq12d  2887  r19.21t  2938  ralbida  2965  ralbidv2  2967  r19.23t  3003  rexbida  3029  rexbidv2  3030  ralcom2  3083  reubida  3101  rmobida  3106  raleqf  3111  rexeqf  3112  reueq1f  3113  rmoeq1f  3114  cbvraldva2  3151  cbvrexdva2  3152  dfsbcq  3404  sbceqbid  3409  sbcbi2  3451  sbcbid  3456  eqsbc3r  3459  sbcrext  3478  sbcrextOLD  3479  sbcabel  3483  psseq1  3656  psseq2  3657  ssconb  3705  uneq1  3722  ineq1  3769  difin2  3849  reuun2  3869  sbcnel12g  3937  sbnfc2  3959  reldisj  3972  undif4  3987  disjssun  3988  pssdifcom1  4006  pssdifcom2  4007  sbcssg  4035  eltpg  4174  raltpg  4183  rextpg  4184  r19.12sn  4199  intmin4  4441  dfiun2g  4488  iindif2  4525  iinin2  4526  disjprg  4578  disjxun  4581  breq  4585  breq1  4586  breq2  4587  treq  4686  reusv2lem5  4799  rexxfrd  4807  rexxfr2d  4809  rexxfrd2  4811  rabxfrd  4815  opthg2  4874  oteqex2  4888  oteqex  4889  poeq1  4962  soeq1  4978  freq1  5008  weeq1  5026  weeq2  5027  opthprc  5089  wesn  5113  releq  5124  sbcrel  5128  eqrel  5132  eqrelrel  5144  xpiindi  5179  brcnvg  5225  brresg  5325  resieq  5327  dmsnopg  5524  dfco2a  5552  ordeq  5647  limeq  5652  ordunisssuc  5747  iotaeq  5776  sniota  5795  sbcfung  5827  imadif  5887  fneq1  5893  fneq2  5894  feq1  5939  feq2  5940  feq3  5941  sbcfng  5955  sbcfg  5956  f1eq1  6009  f1eq2  6010  f1eq3  6011  foeq1  6024  foeq2  6025  foeq3  6026  f1oeq1  6040  f1oeq2  6041  f1oeq3  6042  mpteqb  6207  rexrnmpt  6277  dffo3  6282  fmptco  6303  dff13  6416  f1imaeq  6423  f1imapss  6424  cbvexfo  6445  f1eqcocnv  6456  fliftcnv  6461  isoeq1  6467  isoeq2  6468  isoeq3  6469  isoeq4  6470  isoeq5  6471  isomin  6487  isowe  6499  fnotovb  6592  mpt2eq123  6612  rexrnmpt2  6674  iunpw  6870  tfinds  6951  fun11iun  7019  opiota  7118  ottpos  7249  dmtpos  7251  onoviun  7327  smoeq  7334  smoiso2  7353  tfr2b  7379  oarec  7529  oeeui  7569  nnacan  7595  nnmcan  7601  ereq1  7636  ereq2  7637  elecg  7672  ereldm  7677  ixpiin  7820  boxriin  7836  boxcutc  7837  omxpenlem  7946  nnsdomo  8040  enfi  8061  isfinite2  8103  ixpfi2  8147  elfi2  8203  fipwss  8218  ennum  8656  cardsdom2  8697  aleph11  8790  alephiso  8804  fin23lem26  9030  compssiso  9079  isf34lem4  9082  isfin5-2  9096  fin1a2lem5  9109  brdom7disj  9234  brdom6disj  9235  fpwwe2lem8  9338  fpwwe2lem12  9342  fpwwe2lem13  9343  genpass  9710  ltasr  9800  axpre-lttri  9865  infm3  10861  creur  10891  eqreznegel  11650  rpneg  11739  ltxr  11825  icoshftf1o  12166  elfzm11  12280  elfzomelpfzo  12438  nn0ennn  12640  nnesq  12850  hashbclem  13093  hashf1lem1  13096  leiso  13100  fz1isolem  13102  pr2pwpr  13116  repsdf2  13376  dfrtrclrec2  13645  rexfiuz  13935  cau4  13944  ello1mpt2  14101  o1lo1  14116  fsumcom2  14347  fsumcom2OLD  14348  incexc2  14409  fprodcom2  14553  fprodcom2OLD  14554  dvdsflip  14877  bitsmod  14996  bitscmp  14998  smueqlem  15050  ncoprmgcdne1b  15201  divgcdcoprm0  15217  hashdvds  15318  prmreclem2  15459  vdwapun  15516  vdwmc2  15521  imasaddfnlem  16011  comfeq  16189  oppcsect  16261  funcres2b  16380  funcpropd  16383  fullpropd  16403  fthpropd  16404  fthres2b  16413  fthres2c  16414  fullres2c  16422  ffthres2c  16423  fucsect  16455  fucinv  16456  setcsect  16562  tosso  16859  pospropd  16957  odulatb  16966  oduclatb  16967  isipodrs  16984  odudlatb  17019  issgrpv  17109  issgrpn0  17110  mndpropd  17139  mhmpropd  17164  issubm2  17171  grppropd  17260  grpinvcnv  17306  conjghm  17514  conjnmzb  17518  ghmpropd  17521  gapm  17562  symg1bas  17639  pmtrfrn  17701  cmnpropd  18025  ablpropd  18026  eqgabl  18063  gsumcom2  18197  dmdprd  18220  dprdw  18232  subgdmdprd  18256  pgpfac1lem2  18297  pgpfac1lem4  18300  ringpropd  18405  crngpropd  18406  crngunit  18485  unitpropd  18520  isnirred  18523  drngpropd  18597  fldpropd  18598  subrgpropd  18637  rhmpropd  18638  abvpropd  18665  lmodprop2d  18748  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  lvecprop2d  18987  lvecpropd  18988  opprdomn  19122  fiidomfld  19129  assapropd  19148  psrbagconf1o  19195  mplmonmul  19285  phlpropd  19819  mat1dimbas  20097  tpspropd  20555  tgss2  20602  lmbr2  20873  ist1-2  20961  ist1-3  20963  subislly  21094  dissnlocfin  21142  iskgen3  21162  txcnmpt  21237  hausdiag  21258  hauseqlcld  21259  xkococnlem  21272  tgqtop  21325  txhmeo  21416  uffix2  21538  ufildr  21545  txflf  21620  tgphaus  21730  qustgplem  21734  qustgphaus  21736  xpsdsval  21996  blin  22036  blres  22046  xmeterval  22047  xmspropd  22088  mspropd  22089  setsms  22095  metequiv  22124  metustsym  22170  restmetu  22185  ngppropd  22251  xrtgioo  22417  metdsge  22460  icopnfcnv  22549  iccpnfcnv  22551  lmhmclm  22695  lmmbr  22864  equivcmet  22922  cmspropd  22954  iunmbl2  23132  ioombl1lem4  23136  mbfaddlem  23233  i1fmullem  23267  itg1mulc  23277  iblcnlem1  23360  iblrelem  23363  iblre  23366  iblcn  23371  limcun  23465  mvth  23559  ofmulrt  23841  resinf1o  24086  quad2  24366  1cubr  24369  dcubic  24373  wilthlem2  24595  dvdsflf1o  24713  dvdsflsumcom  24714  fsumvma  24738  vmasum  24741  logfac2  24742  logfaclbnd  24747  dchrelbas3  24763  lgsquadlem1  24905  lgsquadlem2  24906  ax5seg  25618  clwwlknscsh  26347  el2wlkonotot1  26401  2pthwlkonot  26412  rusgranumwlkb0  26480  eupath2lem2  26505  usg2spot2nb  26592  numclwwlkovfel2  26610  ocin  27539  chpsscon3  27746  chscllem2  27881  adjval  28133  pjimai  28419  mdsldmd1i  28574  elat2  28583  mdsymi  28654  sbceqbidf  28705  rmoxfrdOLD  28716  rmoxfrd  28717  disjrdx  28786  eqrelrd2  28806  fmptcof2  28839  ofpreima  28848  funcnv5mpt  28852  1stpreima  28867  2ndpreima  28868  fpwrelmapffslem  28895  smatrcl  29190  locfinreflem  29235  zhmnrg  29339  qqhval2  29354  ismntop  29398  bnj919  30091  bnj956  30101  bnj976  30102  bnj1366  30154  bnj916  30257  dfpo2  30898  dfres3  30902  sscoid  31190  dfrdg4  31228  altopthbg  31245  broutsideof3  31403  bj-nfbi  31793  bj-ssbequ  31818  bj-cbvexdv  31923  bj-drex1v  31937  bj-drnf1v  31938  bj-nfbiit  32024  bj-eleq1w  32040  bj-eleq2w  32041  bj-ax8  32080  bj-restuni  32231  wl-nanbi1  32479  wl-nanbi2  32480  wl-sb8eut  32538  wl-sb8mot  32539  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem25  32604  ftc1anclem5  32659  istotbnd3  32740  sstotbnd  32744  heibor  32790  isass  32815  isidlc  32984  smprngopr  33021  islshpsm  33285  lcvexchlem1  33339  opcon1b  33503  isat3  33612  glbconN  33681  cdleme32fva  34743  cdlemg2cex  34897  dibelval3  35454  dib1dim  35472  doch11  35680  dochsordN  35681  mapdordlem1a  35941  mapd11  35946  mapdsord  35962  mapdcnv11N  35966  mapd0  35972  mrefg2  36288  jm2.23  36581  wepwsolem  36630  dnwech  36636  islssfg2  36659  gicabl  36687  acsfn1p  36788  isdomn3  36801  ifpbi2  36830  ifpbi3  36831  ifpbi23  36836  ifpbi1  36841  ifpbi12  36852  ifpbi13  36853  ifpbi123  36854  pwinfig  36885  inintabd  36904  cnvcnvintabd  36925  cnvintabd  36928  intimag  36967  briunov2  36993  heeq12  37090  sbcheg  37093  rcompleq  37338  uneqsn  37341  ntrneineine0lem  37401  ntrneineine1lem  37402  ntrneik2  37410  ntrneix2  37411  ntrneik13  37416  ntrneix13  37417  ralbidar  37670  rexbidar  37671  trsbc  37771  dffo3f  38359  iccintsng  38596  dfateq12d  39858  aov0nbovbi  39924  fnotaovb  39927  ushgredgedga  40456  ushgredgedgaloop  40458  nbumgrvtx  40568  rusgrnumwwlkb0  41174  isclwwlksnx  41197  clwwlksnscsh  41247  0clWlk  41298  eupth2lem2  41387  eucrct2eupth  41413  fusgr2wsp2nb  41498  av-numclwwlkovfel2  41514  mgmhmpropd  41575  rngcsect  41772  rngcsectALTV  41784  ringcsect  41823  ringcsectALTV  41847  lindslinindsimp2lem5  42045
  Copyright terms: Public domain W3C validator