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

Theorem 3bitr4g 317
Description: More general version of 3bitr4i 306. 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 286 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 292 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  bibi1d  347  pm5.32rd  581  orbi2d  913  orbi1d  914  ifpbi123d  1075  ifpbi123dOLD  1076  3orbi123d  1432  3anbi123d  1433  nanbi1  1492  nanbi2  1493  xorbi12d  1518  hadbi123d  1596  had0  1606  cadbi123d  1612  nfbiit  1852  nfbidv  1924  sbequ  2091  nfbidf  2227  drex1v  2389  drnf1v  2390  drex1  2464  drnf1  2466  sb4b  2500  sb4bOLD  2501  drsb1  2536  eujustALT  2657  eubi  2669  eleq1ab  2801  eqeq1d  2823  eqeq1dALT  2824  eqeq2d  2832  abbi1  2884  eleq1w  2894  eleq2w  2895  eleq1d  2896  eleq2d  2897  eleq2dALT  2898  abbi2dv  2949  nfceqdf  2969  drnfc1  2993  drnfc2  2994  neleq12d  3115  ralbidv2  3183  r19.21t  3202  ralbida  3218  rexbidv2  3281  r19.23t  3299  rexbida  3304  ralrexbid  3308  ralcom2  3348  reubida  3372  reubidva  3373  rmobida  3377  raleqf  3382  rexeqf  3383  reueq1f  3384  rmoeq1f  3385  reueq1  3392  rmoeq1  3393  cbvraldva2  3433  cbvrexdva2  3434  cbvrexdva2OLD  3435  dfsbcq  3751  sbceqbid  3756  sbcbid  3802  sbcbi2  3807  eqsbc3r  3813  sbcrext  3831  sbcabel  3836  psseq1  4040  psseq2  4041  ssconb  4090  uneq1  4108  ineq1OLD  4157  difin2  4241  reuun2  4261  sbcnel12g  4336  sbnfc2  4361  reldisj  4375  undif4  4389  disjssun  4390  pssdifcom1  4408  pssdifcom2  4409  sbcssg  4436  eltpg  4596  raltpg  4607  rextpg  4608  r19.12sn  4629  intmin4  4878  dfiun2g  4928  dfiun2gOLD  4929  iindif1  4970  iindif2  4972  iinin2  4973  disjprgw  5034  disjprg  5035  disjxun  5037  breq  5041  breq1  5042  breq2  5043  treq  5151  reusv2lem5  5276  rexxfrd  5283  rexxfr2d  5285  rexxfrd2  5287  rabxfrd  5291  opthg2  5344  oteqex2  5362  oteqex  5363  poeq1  5450  soeq1  5467  freq1  5498  weeq1  5516  weeq2  5517  opthprc  5589  wesn  5613  releq  5624  sbcrel  5628  eqrel  5631  eqrelrel  5643  xpiindi  5679  dmopab2rex  5759  dfres3  5831  brres  5833  resieq  5837  dmsnopg  6043  dfco2a  6072  ordeq  6171  limeq  6176  ordunisssuc  6266  iotaeq  6299  sniota  6319  sbcfung  6352  imadif  6411  fneq1  6417  fneq2  6418  feq1  6468  feq2  6469  feq3  6470  sbcfng  6484  sbcfg  6485  f1eq1  6543  f1eq2  6544  f1eq3  6545  foeq1  6559  foeq2  6560  foeq3  6561  f1oeq1  6577  f1oeq2  6578  f1oeq3  6579  mpteqb  6760  rexrnmptw  6834  rexrnmpt  6836  dffo3  6841  fmptco  6864  dff13  6987  f1imaeq  6997  f1imapss  6998  cbvexfo  7020  f1eqcocnv  7031  fliftcnv  7038  isoeq1  7044  isoeq2  7045  isoeq3  7046  isoeq4  7047  isoeq5  7048  isomin  7064  isowe  7076  nfriotadw  7096  mpoeq123  7200  rexrnmpo  7264  iunpw  7468  tfinds  7549  fiun  7619  f1iun  7620  opiota  7732  ottpos  7877  dmtpos  7879  onoviun  7955  smoeq  7962  smoiso2  7981  tfr2b  8007  oarec  8163  oeeui  8203  nnacan  8229  nnmcan  8235  ereq1  8271  ereq2  8272  elecg  8307  ereldm  8312  ixpiin  8463  boxriin  8479  boxcutc  8480  omxpenlem  8593  nnsdomo  8690  enfi  8710  isfinite2  8752  ixpfi2  8798  elfi2  8854  fipwss  8869  ennum  9352  cardsdom2  9393  aleph11  9487  alephiso  9501  fin23lem26  9724  compssiso  9773  isf34lem4  9776  isfin5-2  9790  fin1a2lem5  9803  brdom7disj  9930  brdom6disj  9931  fpwwe2lem8  10036  fpwwe2lem12  10040  fpwwe2lem13  10041  genpass  10408  ltasr  10499  axpre-lttri  10564  infm3  11577  creur  11609  eqreznegel  12312  rpneg  12399  ltxr  12488  icoshftf1o  12842  elfzm11  12961  elfzomelpfzo  13124  nn0ennn  13330  nnesq  13572  hashbclem  13794  hashf1lem1  13797  leiso  13801  fz1isolem  13803  pr2pwpr  13821  repsdf2  14119  dfrtrclrec2  14395  rexfiuz  14686  cau4  14695  ello1mpt2  14858  o1lo1  14873  fsumcom2  15108  incexc2  15172  fprodcom2  15317  dvdsflip  15646  bitsmod  15762  bitscmp  15764  smueqlem  15816  divgcdcoprm0  15986  hashdvds  16089  prmreclem2  16230  vdwapun  16287  vdwmc2  16292  imasaddfnlem  16779  comfeq  16954  oppcsect  17026  funcres2b  17145  funcpropd  17148  fullpropd  17168  fthpropd  17169  fthres2b  17178  fthres2c  17179  fullres2c  17187  ffthres2c  17188  fucsect  17220  fucinv  17221  setcsect  17327  tosso  17624  pospropd  17722  odulatb  17731  oduclatb  17732  isipodrs  17749  odudlatb  17784  issgrpv  17881  issgrpn0  17882  mndpropd  17914  mhmpropd  17940  issubm2  17947  efmnd1bas  18036  grppropd  18096  grpinvcnv  18145  conjghm  18367  conjnmzb  18371  ghmpropd  18374  gapm  18414  symg1bas  18497  pmtrfrn  18564  cmnpropd  18894  ablpropd  18895  eqgabl  18933  gsumcom2  19073  dmdprd  19098  dprdw  19110  subgdmdprd  19134  pgpfac1lem2  19175  pgpfac1lem4  19178  ringpropd  19310  crngpropd  19311  crngunit  19390  unitpropd  19425  isnirred  19428  drngpropd  19504  fldpropd  19505  subrgpropd  19545  rhmpropd  19546  acsfn1p  19553  abvpropd  19588  lmodprop2d  19671  lsspropd  19764  lmhmpropd  19820  lbspropd  19846  lvecprop2d  19913  lvecpropd  19914  opprdomn  20049  fiidomfld  20056  assapropd  20076  psrbagconf1o  20129  mplmonmul  20220  phlpropd  20774  mat1dimbas  21056  tpspropd  21521  tgss2  21570  lmbr2  21842  ist1-2  21930  ist1-3  21932  subislly  22064  dissnlocfin  22112  iskgen3  22132  txcnmpt  22207  hausdiag  22228  hauseqlcld  22229  xkococnlem  22242  tgqtop  22295  txhmeo  22386  uffix2  22507  ufildr  22514  txflf  22589  tgphaus  22700  qustgplem  22704  qustgphaus  22706  xpsdsval  22966  blin  23006  blres  23016  xmeterval  23017  xmspropd  23058  mspropd  23059  setsms  23065  metequiv  23094  metustsym  23140  restmetu  23155  ngppropd  23221  xrtgioo  23389  metdsge  23432  icopnfcnv  23525  iccpnfcnv  23527  lmhmclm  23670  lmmbr  23840  equivcmet  23899  cmspropd  23931  iunmbl2  24139  ioombl1lem4  24143  mbfaddlem  24242  i1fmullem  24276  itg1mulc  24286  iblcnlem1  24369  iblrelem  24372  iblre  24375  iblcn  24380  limcun  24476  mvth  24573  ofmulrt  24856  resinf1o  25106  quad2  25403  1cubr  25406  dcubic  25410  wilthlem2  25632  dvdsflf1o  25750  dvdsflsumcom  25751  fsumvma  25775  vmasum  25778  logfac2  25779  logfaclbnd  25784  dchrelbas3  25800  lgsquadlem1  25942  lgsquadlem2  25943  ax5seg  26710  ushgredgedg  26997  ushgredgedgloop  26999  nbumgrvtx  27114  upgriswlk  27408  wspniunwspnon  27687  rusgrnumwwlkb0  27735  isclwwlknx  27799  clwwlknscsh  27825  clwwlknonel  27858  0trl  27885  0spth  27889  0clwlk  27893  0crct  27896  0cycl  27897  eupth2lem2  27982  eucrct2eupth  28008  fusgr2wsp2nb  28097  ocin  29057  chpsscon3  29264  chscllem2  29399  adjval  29651  pjimai  29937  mdsldmd1i  30092  elat2  30101  mdsymi  30172  sbceqbidf  30234  rmoxfrd  30241  rmounid  30243  disjxun0  30310  disjrdx  30327  eqrelrd2  30353  fmptcof2  30388  ofpreima  30396  funcnv5mpt  30399  1stpreima  30428  2ndpreima  30429  fpwrelmapffslem  30454  qsxpid  30934  smatrcl  31071  locfinreflem  31114  zhmnrg  31215  qqhval2  31230  ismntop  31274  reprsuc  31893  reprdifc  31905  bnj919  32045  bnj956  32055  bnj976  32056  bnj1366  32108  bnj916  32212  satfvsucsuc  32619  satfdm  32623  dmopab3rexdif  32659  dfpo2  32998  eqfunresadj  33011  sscoid  33381  dfrdg4  33419  altopthbg  33436  broutsideof3  33594  bj-nnfbi  34064  bj-cbvexdv  34129  bj-sbievw  34178  mobidvALT  34188  bj-restuni  34404  bj-elid6  34478  cbveud  34671  cbvreud  34672  exrecfnlem  34678  wl-3xorbi123d  34770  wl-sb8eut  34858  wl-sb8mot  34859  wl-clabtv  34874  wl-clabt  34875  wl-dfralf  34884  wl-dfrexf  34892  wl-dfrmof  34900  wl-dfreuf  34904  wl-dfrabf  34909  poimirlem17  34954  poimirlem19  34956  poimirlem20  34957  poimirlem25  34962  ftc1anclem5  35014  istotbnd3  35089  sstotbnd  35093  heibor  35139  isass  35164  isidlc  35333  smprngopr  35370  brvvdif  35564  elecALTV  35567  eqrel2  35597  dmecd  35602  relcnveq2  35620  elrelscnveq2  35773  extssr  35789  elrefrelsrel  35799  refreleq  35800  elcnvrefrelsrel  35812  elsymrelsrel  35833  symreleq  35834  eltrrelsrel  35857  trreleq  35858  eleqvrelsrel  35869  eqvreleq  35877  redundpim3  35905  erALTVeq1  35943  elfunsALTVfunALTV  35970  eldisjsdisj  36000  eldisjeq  36014  islshpsm  36156  lcvexchlem1  36210  opcon1b  36374  isat3  36483  glbconN  36553  cdleme32fva  37613  cdlemg2cex  37767  dibelval3  38323  dib1dim  38341  doch11  38549  dochsordN  38550  mapdordlem1a  38810  mapd11  38815  mapdsord  38831  mapdcnv11N  38835  mapd0  38841  lmhmlvec  39272  mrefg2  39445  jm2.23  39734  wepwsolem  39783  dnwech  39789  islssfg2  39812  gicabl  39840  isdomn3  39945  ifpbi2  39972  ifpbi3  39973  ifpbi23  39978  ifpbi1  39982  ifpbi12  39993  ifpbi13  39994  ontric3g  40027  pwinfig  40057  inintabd  40076  cnvcnvintabd  40097  cnvintabd  40100  intimag  40138  briunov2  40164  heeq12  40259  sbcheg  40262  rcompleq  40507  uneqsn  40510  ntrneineine0lem  40570  ntrneineine1lem  40571  ntrneik2  40579  ntrneix2  40580  ntrneik13  40585  ntrneix13  40586  ralbidar  40934  rexbidar  40935  trsbc  41031  rnmptpr  41589  dffo3f  41594  iccintsng  41953  xlimres  42256  dfateq12d  43475  aov0nbovbi  43544  fnotaovb  43547  ichbidv  43763  sprsymrelf  43805  prprsprreu  43829  prprreueq  43830  mgmhmpropd  44199  rngcsect  44398  rngcsectALTV  44410  ringcsect  44449  ringcsectALTV  44473  lindslinindsimp2lem5  44664
  Copyright terms: Public domain W3C validator