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

Theorem 3bitr4g 305
Description: More general version of 3bitr4i 294. 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 274 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 280 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  bibi1d  334  pm5.32rd  569  orbi2d  930  orbi1d  931  ifpbi123d  1093  3orbi123d  1552  3anbi123d  1553  nanbi1  1609  nanbi2  1610  xorbi12d  1632  hadbi123d  1689  had0  1698  cadbi123d  1704  nfbiit  1936  nfbidv  2013  19.23t  2247  nfbidf  2261  nfbidfOLD  2377  19.23tOLD  2394  drex1  2491  drnf1  2493  drsb1  2538  mobidv  2636  eujustALT  2644  eubidv  2647  eubidvOLDOLD  2648  mobidvOLDOLD  2649  eubid  2662  mobid  2663  eqeq1d  2819  eqeq1dALT  2820  eqeq2d  2827  eleq1w  2879  eleq2w  2880  eleq1d  2881  eleq2d  2882  eleq2dALT  2883  nfceqdf  2955  drnfc1  2977  drnfc2  2978  neleq12d  3096  r19.21t  3154  ralbida  3181  ralbidv2  3183  r19.23t  3220  rexbida  3246  rexbidv2  3247  ralcom2  3303  reubida  3324  rmobida  3329  raleqf  3334  rexeqf  3335  reueq1f  3336  rmoeq1f  3337  cbvraldva2  3375  cbvrexdva2  3376  dfsbcq  3646  sbceqbid  3651  sbcbi2  3693  sbcbid  3698  eqsbc3r  3701  sbcrext  3718  sbcabel  3723  psseq1  3903  psseq2  3904  ssconb  3953  uneq1  3970  ineq1  4017  difin2  4102  reuun2  4122  sbcnel12g  4193  sbnfc2  4216  reldisj  4228  undif4  4242  disjssun  4243  pssdifcom1  4261  pssdifcom2  4262  sbcssg  4289  eltpg  4430  raltpg  4439  rextpg  4440  r19.12sn  4457  intmin4  4709  dfiun2g  4755  iindif2  4792  iinin2  4793  disjprg  4851  disjxun  4853  breq  4857  breq1  4858  breq2  4859  treq  4963  reusv2lem5  5084  rexxfrd  5091  rexxfr2d  5093  rexxfrd2  5095  rabxfrd  5099  opthg2  5150  oteqex2  5165  oteqex  5166  poeq1  5248  soeq1  5264  freq1  5294  weeq1  5312  weeq2  5313  opthprc  5380  wesn  5405  releq  5416  sbcrel  5420  eqrel  5424  eqrelrel  5436  xpiindi  5472  brcnvg  5517  dfres3  5615  brresg  5617  resieq  5624  dmsnopg  5831  dfco2a  5862  ordeq  5956  limeq  5961  ordunisssuc  6052  iotaeq  6081  sniota  6100  sbcfung  6134  imadif  6193  fneq1  6199  fneq2  6200  feq1  6246  feq2  6247  feq3  6248  sbcfng  6262  sbcfg  6263  f1eq1  6320  f1eq2  6321  f1eq3  6322  foeq1  6336  foeq2  6337  foeq3  6338  f1oeq1  6352  f1oeq2  6353  f1oeq3  6354  mpteqb  6529  rexrnmpt  6600  dffo3  6605  fmptco  6628  dff13  6745  f1imaeq  6755  f1imapss  6756  cbvexfo  6778  f1eqcocnv  6789  fliftcnv  6794  isoeq1  6800  isoeq2  6801  isoeq3  6802  isoeq4  6803  isoeq5  6804  isomin  6820  isowe  6832  fnotovbOLD  6933  mpt2eq123  6953  rexrnmpt2  7015  iunpw  7217  tfinds  7298  fun11iun  7365  opiota  7470  ottpos  7606  dmtpos  7608  onoviun  7685  smoeq  7692  smoiso2  7711  tfr2b  7737  oarec  7888  oeeui  7928  nnacan  7954  nnmcan  7960  ereq1  7995  ereq2  7996  elecg  8029  ereldm  8034  ixpiin  8180  boxriin  8196  boxcutc  8197  omxpenlem  8309  nnsdomo  8403  enfi  8424  isfinite2  8466  ixpfi2  8512  elfi2  8568  fipwss  8583  ennum  9065  cardsdom2  9106  aleph11  9199  alephiso  9213  fin23lem26  9441  compssiso  9490  isf34lem4  9493  isfin5-2  9507  fin1a2lem5  9520  brdom7disj  9647  brdom6disj  9648  fpwwe2lem8  9753  fpwwe2lem12  9757  fpwwe2lem13  9758  genpass  10125  ltasr  10215  axpre-lttri  10280  infm3  11276  creur  11308  eqreznegel  12012  rpneg  12096  ltxr  12184  icoshftf1o  12535  elfzm11  12653  elfzomelpfzo  12815  nn0ennn  13021  nnesq  13230  hashbclem  13472  hashf1lem1  13475  leiso  13479  fz1isolem  13481  pr2pwpr  13497  repsdf2  13768  dfrtrclrec2  14039  rexfiuz  14329  cau4  14338  ello1mpt2  14495  o1lo1  14510  fsumcom2  14747  incexc2  14811  fprodcom2  14954  dvdsflip  15281  bitsmod  15396  bitscmp  15398  smueqlem  15450  ncoprmgcdne1b  15601  divgcdcoprm0  15616  hashdvds  15716  prmreclem2  15857  vdwapun  15914  vdwmc2  15919  imasaddfnlem  16412  comfeq  16589  oppcsect  16661  funcres2b  16780  funcpropd  16783  fullpropd  16803  fthpropd  16804  fthres2b  16813  fthres2c  16814  fullres2c  16822  ffthres2c  16823  fucsect  16855  fucinv  16856  setcsect  16962  tosso  17260  pospropd  17358  odulatb  17367  oduclatb  17368  isipodrs  17385  odudlatb  17420  issgrpv  17510  issgrpn0  17511  mndpropd  17540  mhmpropd  17565  issubm2  17572  grppropd  17661  grpinvcnv  17707  conjghm  17912  conjnmzb  17916  ghmpropd  17919  gapm  17959  symg1bas  18036  pmtrfrn  18098  cmnpropd  18422  ablpropd  18423  eqgabl  18460  gsumcom2  18594  dmdprd  18618  dprdw  18630  subgdmdprd  18654  pgpfac1lem2  18695  pgpfac1lem4  18698  ringpropd  18803  crngpropd  18804  crngunit  18883  unitpropd  18918  isnirred  18921  drngpropd  18997  fldpropd  18998  subrgpropd  19037  rhmpropd  19038  abvpropd  19065  lmodprop2d  19148  lsspropd  19243  lmhmpropd  19299  lbspropd  19325  lvecprop2d  19394  lvecpropd  19395  opprdomn  19529  fiidomfld  19536  assapropd  19555  psrbagconf1o  19602  mplmonmul  19692  phlpropd  20229  mat1dimbas  20509  tpspropd  20976  tgss2  21025  lmbr2  21297  ist1-2  21385  ist1-3  21387  subislly  21518  dissnlocfin  21566  iskgen3  21586  txcnmpt  21661  hausdiag  21682  hauseqlcld  21683  xkococnlem  21696  tgqtop  21749  txhmeo  21840  uffix2  21961  ufildr  21968  txflf  22043  tgphaus  22153  qustgplem  22157  qustgphaus  22159  xpsdsval  22419  blin  22459  blres  22469  xmeterval  22470  xmspropd  22511  mspropd  22512  setsms  22518  metequiv  22547  metustsym  22593  restmetu  22608  ngppropd  22674  xrtgioo  22842  metdsge  22885  icopnfcnv  22974  iccpnfcnv  22976  lmhmclm  23119  lmmbr  23289  equivcmet  23347  cmspropd  23379  iunmbl2  23560  ioombl1lem4  23564  mbfaddlem  23663  i1fmullem  23697  itg1mulc  23707  iblcnlem1  23790  iblrelem  23793  iblre  23796  iblcn  23801  limcun  23895  mvth  23991  ofmulrt  24273  resinf1o  24519  quad2  24802  1cubr  24805  dcubic  24809  wilthlem2  25031  dvdsflf1o  25149  dvdsflsumcom  25150  fsumvma  25174  vmasum  25177  logfac2  25178  logfaclbnd  25183  dchrelbas3  25199  lgsquadlem1  25341  lgsquadlem2  25342  ax5seg  26054  ushgredgedg  26358  ushgredgedgloop  26360  ushgredgedgloopOLD  26361  nbumgrvtx  26480  upgriswlk  26787  wspniunwspnon  27085  rusgrnumwwlkb0  27135  isclwwlknx  27206  clwwlknscsh  27235  clwwlknonel  27284  0trl  27317  0spth  27321  0clwlk  27325  0crct  27328  0cycl  27329  eupth2lem2  27414  eucrct2eupth  27440  fusgr2wsp2nb  27531  ocin  28505  chpsscon3  28712  chscllem2  28847  adjval  29099  pjimai  29385  mdsldmd1i  29540  elat2  29549  mdsymi  29620  sbceqbidf  29671  rmoxfrdOLD  29680  rmoxfrd  29681  disjrdx  29751  eqrelrd2  29775  fmptcof2  29806  ofpreima  29814  funcnv5mpt  29818  1stpreima  29833  2ndpreima  29834  fpwrelmapffslem  29856  smatrcl  30209  locfinreflem  30254  zhmnrg  30358  qqhval2  30373  ismntop  30417  reprsuc  31040  reprdifc  31052  bnj919  31181  bnj956  31191  bnj976  31192  bnj1366  31244  bnj916  31347  dfpo2  31988  eqfunresadj  32002  sscoid  32362  dfrdg4  32400  altopthbg  32417  broutsideof3  32575  bj-ssbequ  32966  bj-cbvexdv  33071  bj-drex1v  33084  bj-drnf1v  33085  bj-ax8  33213  bj-restuni  33379  wl-nanbi1  33634  wl-nanbi2  33635  wl-sb8eut  33691  wl-sb8mot  33692  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem25  33765  ftc1anclem5  33819  istotbnd3  33899  sstotbnd  33903  heibor  33949  isass  33974  isidlc  34143  smprngopr  34180  brvvdif  34363  elecALTV  34366  brresALTV  34368  eqrel2  34403  dmecd  34408  relcnveq2  34427  elrelscnveq2  34574  extssr  34590  elrefrelsrel  34600  refreleq  34601  elcnvrefrelsrel  34613  elsymrelsrel  34634  symreleq  34635  islshpsm  34778  lcvexchlem1  34832  opcon1b  34996  isat3  35105  glbconN  35175  cdleme32fva  36235  cdlemg2cex  36389  dibelval3  36945  dib1dim  36963  doch11  37171  dochsordN  37172  mapdordlem1a  37432  mapd11  37437  mapdsord  37453  mapdcnv11N  37457  mapd0  37463  mrefg2  37789  jm2.23  38081  wepwsolem  38130  dnwech  38136  islssfg2  38159  gicabl  38187  acsfn1p  38287  isdomn3  38300  ifpbi2  38328  ifpbi3  38329  ifpbi23  38334  ifpbi1  38339  ifpbi12  38350  ifpbi13  38351  ifpbi123  38352  pwinfig  38383  inintabd  38402  cnvcnvintabd  38423  cnvintabd  38426  intimag  38465  briunov2  38491  heeq12  38587  sbcheg  38590  rcompleq  38835  uneqsn  38838  ntrneineine0lem  38898  ntrneineine1lem  38899  ntrneik2  38907  ntrneix2  38908  ntrneik13  38913  ntrneix13  38914  ralbidar  39164  rexbidar  39165  trsbc  39265  sbcssOLD  39271  dffo3f  39870  iccintsng  40247  xlimres  40544  dfateq12d  41732  aov0nbovbi  41801  fnotaovb  41804  sprsymrelf  42330  mgmhmpropd  42370  rngcsect  42565  rngcsectALTV  42577  ringcsect  42616  ringcsectALTV  42640  lindslinindsimp2lem5  42836
  Copyright terms: Public domain W3C validator