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

Theorem 3bitr4g 303
Description: More general version of 3bitr4i 292. 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 272 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 278 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  bibi1d  333  pm5.32rd  671  orbi2d  737  orbi1d  738  ifpbi123d  1026  3orbi123d  1396  3anbi123d  1397  nanbi1  1453  nanbi2  1454  xorbi12d  1476  hadbi123d  1532  had0  1541  cadbi123d  1547  nfbiit  1775  19.23t  2077  nfbidf  2090  nfbidfOLD  2199  19.23tOLD  2216  cbvexd  2276  drex1  2325  drnf1  2327  drsb1  2375  eujustALT  2471  eubid  2486  mobid  2487  eqeq1d  2622  eqeq1dALT  2623  eqeq2d  2630  eleq1w  2682  eleq2w  2683  eleq1d  2684  eleq2d  2685  eleq2dALT  2686  nfceqdf  2758  drnfc1  2779  drnfc2  2780  neleq12d  2898  r19.21t  2952  ralbida  2979  ralbidv2  2981  r19.23t  3017  rexbida  3043  rexbidv2  3044  ralcom2  3099  reubida  3119  rmobida  3124  raleqf  3129  rexeqf  3130  reueq1f  3131  rmoeq1f  3132  cbvraldva2  3170  cbvrexdva2  3171  dfsbcq  3431  sbceqbid  3436  sbcbi2  3478  sbcbid  3483  eqsbc3r  3486  sbcrext  3505  sbcrextOLD  3506  sbcabel  3510  psseq1  3686  psseq2  3687  ssconb  3735  uneq1  3752  ineq1  3799  difin2  3882  reuun2  3902  sbcnel12g  3976  sbnfc2  3998  reldisj  4011  undif4  4026  disjssun  4027  pssdifcom1  4045  pssdifcom2  4046  sbcssg  4076  eltpg  4218  raltpg  4227  rextpg  4228  r19.12sn  4246  intmin4  4497  dfiun2g  4543  iindif2  4580  iinin2  4581  disjprg  4639  disjxun  4642  breq  4646  breq1  4647  breq2  4648  treq  4749  reusv2lem5  4864  rexxfrd  4872  rexxfr2d  4874  rexxfrd2  4876  rabxfrd  4880  opthg2  4938  oteqex2  4953  oteqex  4954  poeq1  5028  soeq1  5044  freq1  5074  weeq1  5092  weeq2  5093  opthprc  5157  wesn  5180  releq  5191  sbcrel  5195  eqrel  5199  eqrelrel  5211  xpiindi  5246  brcnvg  5292  brresg  5393  resieq  5395  dmsnopg  5594  dfco2a  5623  ordeq  5718  limeq  5723  ordunisssuc  5818  iotaeq  5847  sniota  5866  sbcfung  5900  imadif  5961  fneq1  5967  fneq2  5968  feq1  6013  feq2  6014  feq3  6015  sbcfng  6029  sbcfg  6030  f1eq1  6083  f1eq2  6084  f1eq3  6085  foeq1  6098  foeq2  6099  foeq3  6100  f1oeq1  6114  f1oeq2  6115  f1oeq3  6116  mpteqb  6285  rexrnmpt  6355  dffo3  6360  fmptco  6382  dff13  6497  f1imaeq  6507  f1imapss  6508  cbvexfo  6530  f1eqcocnv  6541  fliftcnv  6546  isoeq1  6552  isoeq2  6553  isoeq3  6554  isoeq4  6555  isoeq5  6556  isomin  6572  isowe  6584  fnotovb  6679  mpt2eq123  6699  rexrnmpt2  6761  iunpw  6963  tfinds  7044  fun11iun  7111  opiota  7214  ottpos  7347  dmtpos  7349  onoviun  7425  smoeq  7432  smoiso2  7451  tfr2b  7477  oarec  7627  oeeui  7667  nnacan  7693  nnmcan  7699  ereq1  7734  ereq2  7735  elecg  7770  ereldm  7775  ixpiin  7919  boxriin  7935  boxcutc  7936  omxpenlem  8046  nnsdomo  8140  enfi  8161  isfinite2  8203  ixpfi2  8249  elfi2  8305  fipwss  8320  ennum  8758  cardsdom2  8799  aleph11  8892  alephiso  8906  fin23lem26  9132  compssiso  9181  isf34lem4  9184  isfin5-2  9198  fin1a2lem5  9211  brdom7disj  9338  brdom6disj  9339  fpwwe2lem8  9444  fpwwe2lem12  9448  fpwwe2lem13  9449  genpass  9816  ltasr  9906  axpre-lttri  9971  infm3  10967  creur  10999  eqreznegel  11759  rpneg  11848  ltxr  11934  icoshftf1o  12280  elfzm11  12395  elfzomelpfzo  12556  nn0ennn  12761  nnesq  12971  hashbclem  13219  hashf1lem1  13222  leiso  13226  fz1isolem  13228  pr2pwpr  13244  repsdf2  13506  dfrtrclrec2  13778  rexfiuz  14068  cau4  14077  ello1mpt2  14234  o1lo1  14249  fsumcom2  14486  fsumcom2OLD  14487  incexc2  14551  fprodcom2  14695  fprodcom2OLD  14696  dvdsflip  15020  bitsmod  15139  bitscmp  15141  smueqlem  15193  ncoprmgcdne1b  15344  divgcdcoprm0  15360  hashdvds  15461  prmreclem2  15602  vdwapun  15659  vdwmc2  15664  imasaddfnlem  16169  comfeq  16347  oppcsect  16419  funcres2b  16538  funcpropd  16541  fullpropd  16561  fthpropd  16562  fthres2b  16571  fthres2c  16572  fullres2c  16580  ffthres2c  16581  fucsect  16613  fucinv  16614  setcsect  16720  tosso  17017  pospropd  17115  odulatb  17124  oduclatb  17125  isipodrs  17142  odudlatb  17177  issgrpv  17267  issgrpn0  17268  mndpropd  17297  mhmpropd  17322  issubm2  17329  grppropd  17418  grpinvcnv  17464  conjghm  17672  conjnmzb  17676  ghmpropd  17679  gapm  17720  symg1bas  17797  pmtrfrn  17859  cmnpropd  18183  ablpropd  18184  eqgabl  18221  gsumcom2  18355  dmdprd  18378  dprdw  18390  subgdmdprd  18414  pgpfac1lem2  18455  pgpfac1lem4  18458  ringpropd  18563  crngpropd  18564  crngunit  18643  unitpropd  18678  isnirred  18681  drngpropd  18755  fldpropd  18756  subrgpropd  18795  rhmpropd  18796  abvpropd  18823  lmodprop2d  18906  lsspropd  18998  lmhmpropd  19054  lbspropd  19080  lvecprop2d  19147  lvecpropd  19148  opprdomn  19282  fiidomfld  19289  assapropd  19308  psrbagconf1o  19355  mplmonmul  19445  phlpropd  19981  mat1dimbas  20259  tpspropd  20723  tgss2  20772  lmbr2  21044  ist1-2  21132  ist1-3  21134  subislly  21265  dissnlocfin  21313  iskgen3  21333  txcnmpt  21408  hausdiag  21429  hauseqlcld  21430  xkococnlem  21443  tgqtop  21496  txhmeo  21587  uffix2  21709  ufildr  21716  txflf  21791  tgphaus  21901  qustgplem  21905  qustgphaus  21907  xpsdsval  22167  blin  22207  blres  22217  xmeterval  22218  xmspropd  22259  mspropd  22260  setsms  22266  metequiv  22295  metustsym  22341  restmetu  22356  ngppropd  22422  xrtgioo  22590  metdsge  22633  icopnfcnv  22722  iccpnfcnv  22724  lmhmclm  22868  lmmbr  23037  equivcmet  23095  cmspropd  23127  iunmbl2  23306  ioombl1lem4  23310  mbfaddlem  23408  i1fmullem  23442  itg1mulc  23452  iblcnlem1  23535  iblrelem  23538  iblre  23541  iblcn  23546  limcun  23640  mvth  23736  ofmulrt  24018  resinf1o  24263  quad2  24547  1cubr  24550  dcubic  24554  wilthlem2  24776  dvdsflf1o  24894  dvdsflsumcom  24895  fsumvma  24919  vmasum  24922  logfac2  24923  logfaclbnd  24928  dchrelbas3  24944  lgsquadlem1  25086  lgsquadlem2  25087  ax5seg  25799  ushgredgedg  26102  ushgredgedgloop  26104  nbumgrvtx  26223  upgriswlk  26518  rusgrnumwwlkb0  26847  isclwwlksnx  26870  clwwlksnscsh  26920  0trl  26963  0spth  26967  0clwlk  26971  0crct  26973  0cycl  26974  eupth2lem2  27059  eucrct2eupth  27085  fusgr2wsp2nb  27172  numclwwlkovfel2  27188  ocin  28125  chpsscon3  28332  chscllem2  28467  adjval  28719  pjimai  29005  mdsldmd1i  29160  elat2  29169  mdsymi  29240  sbceqbidf  29293  rmoxfrdOLD  29304  rmoxfrd  29305  disjrdx  29376  eqrelrd2  29398  fmptcof2  29430  ofpreima  29439  funcnv5mpt  29443  1stpreima  29458  2ndpreima  29459  fpwrelmapffslem  29481  smatrcl  29836  locfinreflem  29881  zhmnrg  29985  qqhval2  30000  ismntop  30044  reprsuc  30667  reprdifc  30679  bnj919  30811  bnj956  30821  bnj976  30822  bnj1366  30874  bnj916  30977  dfpo2  31620  dfres3  31624  eqfunresadj  31635  sscoid  31995  dfrdg4  32033  altopthbg  32050  broutsideof3  32208  bj-ssbequ  32604  bj-cbvexdv  32711  bj-drex1v  32724  bj-drnf1v  32725  bj-ax8  32862  bj-restuni  33025  wl-nanbi1  33271  wl-nanbi2  33272  wl-sb8eut  33330  wl-sb8mot  33331  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem25  33405  ftc1anclem5  33460  istotbnd3  33541  sstotbnd  33545  heibor  33591  isass  33616  isidlc  33785  smprngopr  33822  islshpsm  34086  lcvexchlem1  34140  opcon1b  34304  isat3  34413  glbconN  34482  cdleme32fva  35544  cdlemg2cex  35698  dibelval3  36255  dib1dim  36273  doch11  36481  dochsordN  36482  mapdordlem1a  36742  mapd11  36747  mapdsord  36763  mapdcnv11N  36767  mapd0  36773  mrefg2  37089  jm2.23  37382  wepwsolem  37431  dnwech  37437  islssfg2  37460  gicabl  37488  acsfn1p  37588  isdomn3  37601  ifpbi2  37630  ifpbi3  37631  ifpbi23  37636  ifpbi1  37641  ifpbi12  37652  ifpbi13  37653  ifpbi123  37654  pwinfig  37685  inintabd  37704  cnvcnvintabd  37725  cnvintabd  37728  intimag  37767  briunov2  37793  heeq12  37890  sbcheg  37893  rcompleq  38138  uneqsn  38141  ntrneineine0lem  38201  ntrneineine1lem  38202  ntrneik2  38210  ntrneix2  38211  ntrneik13  38216  ntrneix13  38217  ralbidar  38469  rexbidar  38470  trsbc  38570  dffo3f  39180  iccintsng  39552  dfateq12d  40972  aov0nbovbi  41038  fnotaovb  41041  sprsymrelf  41510  mgmhmpropd  41550  rngcsect  41745  rngcsectALTV  41757  ringcsect  41796  ringcsectALTV  41820  lindslinindsimp2lem5  42016
  Copyright terms: Public domain W3C validator