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

Theorem 3bitr4g 301
Description: More general version of 3bitr4i 290. 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 270 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 276 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  bibi1d  331  pm5.32rd  669  orbi2d  733  orbi1d  734  ifpbi123d  1020  3orbi123d  1389  3anbi123d  1390  nanbi1  1446  nanbi2  1447  xorbi12d  1469  hadbi123d  1524  had0  1533  cadbi123d  1539  19.23t  2064  nfbidf  2077  nfbidfOLD  2184  19.23tOLD  2201  cbvexd  2261  drex1  2311  drnf1  2313  drsb1  2361  eujustALT  2457  eubid  2472  mobid  2473  eqeq1d  2608  eqeq1dALT  2609  eqeq2d  2616  eleq1d  2668  eleq2d  2669  eleq2dOLD  2670  eleq2dALT  2671  nfceqdf  2743  drnfc1  2764  drnfc2  2765  neleq12d  2883  r19.21t  2934  ralbida  2961  ralbidv2  2963  r19.23t  2999  rexbida  3025  rexbidv2  3026  ralcom2  3079  reubida  3097  rmobida  3102  raleqf  3107  rexeqf  3108  reueq1f  3109  rmoeq1f  3110  cbvraldva2  3147  cbvrexdva2  3148  dfsbcq  3400  sbceqbid  3405  sbcbi2  3447  sbcbid  3452  eqsbc3r  3455  sbcrext  3474  sbcrextOLD  3475  sbcabel  3479  psseq1  3652  psseq2  3653  ssconb  3701  uneq1  3718  ineq1  3765  difin2  3845  reuun2  3865  sbcnel12g  3933  sbnfc2  3955  reldisj  3968  undif4  3983  disjssun  3984  pssdifcom1  4002  pssdifcom2  4003  sbcssg  4031  eltpg  4170  raltpg  4179  rextpg  4180  r19.12sn  4195  intmin4  4432  dfiun2g  4479  iindif2  4516  iinin2  4517  disjprg  4569  disjxun  4572  breq  4576  breq1  4577  breq2  4578  treq  4677  reusv2lem5  4791  rexxfrd  4799  rexxfr2d  4801  rexxfrd2  4803  rabxfrd  4807  opthg2  4865  oteqex2  4879  oteqex  4880  poeq1  4949  soeq1  4965  freq1  4995  weeq1  5013  weeq2  5014  opthprc  5076  wesn  5100  releq  5111  sbcrel  5115  eqrel  5118  eqrelrel  5130  xpiindi  5164  brcnvg  5210  brresg  5309  resieq  5311  dmsnopg  5507  dfco2a  5535  ordeq  5630  limeq  5635  ordunisssuc  5730  iotaeq  5759  sniota  5778  sbcfung  5810  imadif  5870  fneq1  5876  fneq2  5877  feq1  5922  feq2  5923  feq3  5924  sbcfng  5938  sbcfg  5939  f1eq1  5991  f1eq2  5992  f1eq3  5993  foeq1  6006  foeq2  6007  foeq3  6008  f1oeq1  6022  f1oeq2  6023  f1oeq3  6024  mpteqb  6189  rexrnmpt  6259  dffo3  6264  fmptco  6285  dff13  6391  f1imaeq  6398  f1imapss  6399  cbvexfo  6420  f1eqcocnv  6431  fliftcnv  6436  isoeq1  6442  isoeq2  6443  isoeq3  6444  isoeq4  6445  isoeq5  6446  isomin  6462  isowe  6474  fnotovb  6567  mpt2eq123  6587  rexrnmpt2  6649  iunpw  6844  tfinds  6925  fun11iun  6993  opiota  7092  ottpos  7223  dmtpos  7225  onoviun  7301  smoeq  7308  smoiso2  7327  tfr2b  7353  oarec  7503  oeeui  7543  nnacan  7569  nnmcan  7575  ereq1  7610  ereq2  7611  elecg  7646  ereldm  7651  ixpiin  7794  boxriin  7810  boxcutc  7811  omxpenlem  7920  nnsdomo  8014  enfi  8035  isfinite2  8077  ixpfi2  8121  elfi2  8177  fipwss  8192  ennum  8630  cardsdom2  8671  aleph11  8764  alephiso  8778  fin23lem26  9004  compssiso  9053  isf34lem4  9056  isfin5-2  9070  fin1a2lem5  9083  brdom7disj  9208  brdom6disj  9209  fpwwe2lem8  9312  fpwwe2lem12  9316  fpwwe2lem13  9317  genpass  9684  ltasr  9774  axpre-lttri  9839  infm3  10828  creur  10858  eqreznegel  11603  rpneg  11692  ltxr  11781  icoshftf1o  12119  elfzm11  12232  elfzomelpfzo  12390  nn0ennn  12592  nnesq  12802  hashbclem  13042  hashf1lem1  13045  leiso  13049  fz1isolem  13051  pr2pwpr  13063  repsdf2  13319  dfrtrclrec2  13588  rexfiuz  13878  cau4  13887  ello1mpt2  14044  o1lo1  14059  fsumcom2  14290  fsumcom2OLD  14291  incexc2  14352  fprodcom2  14496  fprodcom2OLD  14497  dvdsflip  14820  bitsmod  14939  bitscmp  14941  smueqlem  14993  ncoprmgcdne1b  15144  divgcdcoprm0  15160  hashdvds  15261  prmreclem2  15402  vdwapun  15459  vdwmc2  15464  imasaddfnlem  15954  comfeq  16132  oppcsect  16204  funcres2b  16323  funcpropd  16326  fullpropd  16346  fthpropd  16347  fthres2b  16356  fthres2c  16357  fullres2c  16365  ffthres2c  16366  fucsect  16398  fucinv  16399  setcsect  16505  tosso  16802  pospropd  16900  odulatb  16909  oduclatb  16910  isipodrs  16927  odudlatb  16962  issgrpv  17052  issgrpn0  17053  mndpropd  17082  mhmpropd  17107  issubm2  17114  grppropd  17203  grpinvcnv  17249  conjghm  17457  conjnmzb  17461  ghmpropd  17464  gapm  17505  symg1bas  17582  pmtrfrn  17644  cmnpropd  17968  ablpropd  17969  eqgabl  18006  gsumcom2  18140  dmdprd  18163  dprdw  18175  subgdmdprd  18199  pgpfac1lem2  18240  pgpfac1lem4  18243  ringpropd  18348  crngpropd  18349  crngunit  18428  unitpropd  18463  isnirred  18466  drngpropd  18540  fldpropd  18541  subrgpropd  18580  rhmpropd  18581  abvpropd  18608  lmodprop2d  18691  lsspropd  18781  lmhmpropd  18837  lbspropd  18863  lvecprop2d  18930  lvecpropd  18931  opprdomn  19065  fiidomfld  19072  assapropd  19091  psrbagconf1o  19138  mplmonmul  19228  phlpropd  19761  mat1dimbas  20036  tpspropd  20494  tgss2  20541  lmbr2  20812  ist1-2  20900  ist1-3  20902  subislly  21033  dissnlocfin  21081  iskgen3  21101  txcnmpt  21176  hausdiag  21197  hauseqlcld  21198  xkococnlem  21211  tgqtop  21264  txhmeo  21355  uffix2  21477  ufildr  21484  txflf  21559  tgphaus  21669  qustgplem  21673  qustgphaus  21675  xpsdsval  21934  blin  21974  blres  21984  xmeterval  21985  xmspropd  22026  mspropd  22027  setsms  22033  metequiv  22062  metustsym  22108  restmetu  22123  ngppropd  22186  xrtgioo  22346  metdsge  22388  icopnfcnv  22477  iccpnfcnv  22479  lmhmclm  22623  lmmbr  22779  equivcmet  22836  cmspropd  22868  iunmbl2  23046  ioombl1lem4  23050  mbfaddlem  23147  i1fmullem  23181  itg1mulc  23191  iblcnlem1  23274  iblrelem  23277  iblre  23280  iblcn  23285  limcun  23379  mvth  23473  ofmulrt  23755  resinf1o  24000  quad2  24280  1cubr  24283  dcubic  24287  wilthlem2  24509  dvdsflf1o  24627  dvdsflsumcom  24628  fsumvma  24652  vmasum  24655  logfac2  24656  logfaclbnd  24661  dchrelbas3  24677  lgsquadlem1  24819  lgsquadlem2  24820  ax5seg  25533  clwwlknscsh  26110  el2wlkonotot1  26164  2pthwlkonot  26175  rusgranumwlkb0  26243  eupath2lem2  26268  usg2spot2nb  26355  numclwwlkovfel2  26373  ocin  27342  chpsscon3  27549  chscllem2  27684  adjval  27936  pjimai  28222  mdsldmd1i  28377  elat2  28386  mdsymi  28457  sbceqbidf  28508  rmoxfrdOLD  28519  rmoxfrd  28520  disjrdx  28589  eqrelrd2  28609  fmptcof2  28642  ofpreima  28651  funcnv5mpt  28655  1stpreima  28670  2ndpreima  28671  fpwrelmapffslem  28698  smatrcl  28993  locfinreflem  29038  zhmnrg  29142  qqhval2  29157  ismntop  29201  bnj919  29894  bnj956  29904  bnj976  29905  bnj1366  29957  bnj916  30060  dfpo2  30701  dfres3  30705  sscoid  30993  dfrdg4  31031  altopthbg  31048  broutsideof3  31206  bj-nfbi  31596  bj-ssbequ  31621  bj-cbvexdv  31726  bj-drex1v  31741  bj-drnf1v  31742  bj-eleq1w  31840  bj-eleq2w  31841  bj-ax8  31880  bj-restuni  32031  wl-nanbi1  32279  wl-nanbi2  32280  wl-sb8eut  32338  wl-sb8mot  32339  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem25  32404  ftc1anclem5  32459  istotbnd3  32540  sstotbnd  32544  heibor  32590  isass  32615  isidlc  32784  smprngopr  32821  islshpsm  33085  lcvexchlem1  33139  opcon1b  33303  isat3  33412  glbconN  33481  cdleme32fva  34543  cdlemg2cex  34697  dibelval3  35254  dib1dim  35272  doch11  35480  dochsordN  35481  mapdordlem1a  35741  mapd11  35746  mapdsord  35762  mapdcnv11N  35766  mapd0  35772  mrefg2  36088  jm2.23  36381  wepwsolem  36430  dnwech  36436  islssfg2  36459  gicabl  36487  acsfn1p  36588  isdomn3  36601  ifpbi2  36630  ifpbi3  36631  ifpbi23  36636  ifpbi1  36641  ifpbi12  36652  ifpbi13  36653  ifpbi123  36654  pwinfig  36685  inintabd  36704  cnvcnvintabd  36725  cnvintabd  36728  intimag  36767  briunov2  36793  heeq12  36890  sbcheg  36893  rcompleq  37138  uneqsn  37141  ntrneineine0lem  37201  ntrneineine1lem  37202  ntrneik2  37210  ntrneix2  37211  ntrneik13  37216  ntrneix13  37217  ralbidar  37470  rexbidar  37471  trsbc  37571  dffo3f  38159  iccintsng  38397  dfateq12d  39660  aov0nbovbi  39726  fnotaovb  39729  ushgredgedga  40455  ushgredgedgaloop  40457  nbumgrvtx  40567  rusgrnumwwlkb0  41173  isclwwlksnx  41196  clwwlksnscsh  41246  0clWlk  41297  eupth2lem2  41386  eucrct2eupth  41412  fusgr2wsp2nb  41497  av-numclwwlkovfel2  41513  mgmhmpropd  41574  rngcsect  41771  rngcsectALTV  41783  ringcsect  41822  ringcsectALTV  41846  lindslinindsimp2lem5  42044
  Copyright terms: Public domain W3C validator