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

Theorem simpllr 794
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simpllr ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 475 . 2 ((𝜑𝜓) → 𝜓)
21ad2antrr 757 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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  df-an 384
This theorem is referenced by:  simp-4r  802  fsnex  6416  soisoi  6456  f1o2ndf1  7150  tz7.49  7405  omabs  7592  omxpenlem  7924  fopwdom  7931  findcard3  8066  frfi  8068  finsschain  8134  marypha1lem  8200  wdomtr  8341  cantnfp1  8439  harcard  8665  numacn  8733  infunsdom1  8896  cofsmo  8952  sornom  8960  ssfin4  8993  fin1a2lem11  9093  fin1a2lem13  9095  ttukeylem5  9196  fpwwe2lem13  9321  pwfseq  9343  mulcmpblnr  9749  00id  10063  addid1  10068  cnegex  10069  negeu  10123  add20  10392  ltmul12a  10731  lediv12a  10768  fiminre  10824  cru  10862  qextltlem  11869  xleadd1a  11915  xmullem  11926  xlemul1a  11950  ixxss12  12025  ioodisj  12132  fsuppmapnn0fz  12616  seqf1o  12662  mulexpz  12720  leexp1a  12739  faclbnd  12897  swrdswrdlem  13260  abs3lem  13875  cau3lem  13891  rlim3  14026  ello12  14044  lo1bdd2  14052  elo12  14055  rlimconst  14072  isercoll  14195  climcau  14198  climbdd  14199  summolem2  14243  fsumconst  14313  o1fsum  14335  incexclem  14356  fprodconst  14496  bitsfzo  14944  dvdsmulgcd  15061  pc2dvds  15370  pcz  15372  pcadd  15380  pcfac  15390  vdwmc2  15470  vdwlem2  15473  vdwlem10  15481  vdw  15485  ramcl  15520  sbcie3s  15694  firest  15865  prdsval  15887  mreexd  16074  mreexexlemd  16076  iscat  16105  cidfval  16109  iscatd2  16114  catcocl  16118  catass  16119  catpropd  16141  cidpropd  16142  moni  16168  monpropd  16169  issubc  16267  subccocl  16277  funcco  16303  funcpropd  16332  fullpropd  16352  nati  16387  natpropd  16408  fucpropd  16409  xpcpropd  16620  curfuncf  16650  curf2ndf  16659  yonffthlem  16694  acsfiindd  16949  mndpropd  17088  mhmeql  17136  isgrpinv  17244  dfgrp3lem  17285  mhmmnd  17309  conjnmzb  17467  gass  17506  symgextf  17609  dfod2  17753  gexdvds  17771  sylow3lem2  17815  efgredlem  17932  efgredeu  17937  ghmcmn  18009  oddvdssubg  18030  dprdfcntz  18186  pgpfaclem3  18254  issrg  18279  isring  18323  dvdsrmul1  18425  issubdrg  18577  islmhm2  18808  lmhmeql  18825  lssacsex  18914  issubassa2  19115  opsrval  19244  isphl  19740  uvcf1  19898  lindfmm  19933  scmatmats  20084  smatvscl  20097  mdetunilem7  20191  gsummatr01lem4  20231  m2cpmfo  20328  decpmatmulsumfsupp  20345  pmatcollpw3fi1lem1  20358  pm2mpf1lem  20366  pm2mpf1  20371  mp2pm2mplem4  20381  pm2mpghm  20388  pm2mpmhmlem1  20390  pm2mpmhmlem2  20391  chfacfscmulfsupp  20431  chfacfpmmulfsupp  20435  cctop  20568  neiptoptop  20693  neiptopreu  20695  tgrest  20721  ordtrest2lem  20765  cnss1  20838  cncnp  20842  isnrm3  20921  uncmp  20964  cmpfi  20969  iuncon  20989  1stcrest  21014  subislly  21042  islly2  21045  cldllycmp  21056  lly1stc  21057  llycmpkgen2  21111  kgencn  21117  xkoccn  21180  ptcnplem  21182  pthaus  21199  txhaus  21208  txkgen  21213  xkohaus  21214  xkococnlem  21220  txcon  21250  regr1lem2  21301  kqreglem1  21302  reghmph  21354  nrmhmph  21355  trfil2  21449  ufileu  21481  flimopn  21537  flimcf  21544  fclscf  21587  ufilcmp  21594  cnpfcf  21603  cnextfun  21626  tgpmulg  21655  symgtgp  21663  tgpt0  21680  qustgplem  21682  ustex2sym  21778  ustex3sym  21779  trust  21791  restutop  21799  restutopopn  21800  ustuqtop2  21804  ustuqtop4  21806  utop3cls  21813  utopreg  21814  cstucnd  21846  ucncn  21847  trcfilu  21856  neipcfilu  21858  ismet2  21896  metequiv2  22073  metcnp  22104  metcnp2  22105  metcnpi3  22109  txmetcnp  22110  metustto  22116  metustsym  22118  metust  22121  cfilucfil  22122  metuel2  22128  psmetutop  22130  restmetu  22133  metucn  22134  ngptgp  22198  tngngp  22216  nmoleub  22293  icccmp  22384  reconnlem2  22386  reconn  22387  xmetdcn2  22396  metdseq0  22413  metdscn  22415  elcncf2  22449  cncfmet  22467  cnheibor  22510  nmoleub2lem2  22672  nmoleub3  22675  cvsi  22686  iscfil2  22817  iscfil3  22824  cfilfcls  22825  equivcfil  22850  caubl  22859  bcthlem5  22878  pmltpc  22971  ovollb2  23009  ovoliunnul  23027  ovolicc2lem4  23040  volsup  23076  ioorf  23092  dyadss  23113  dyaddisjlem  23114  mbfposr  23170  cncombf  23176  mbflimsup  23184  i1fmulclem  23220  mbfi1fseqlem4  23236  iblss2  23323  ellimc2  23392  ellimc3  23394  dvnadd  23443  dvmptfsum  23487  dvferm1  23497  dvferm2  23499  fta1g  23676  plyeq0lem  23715  plydivex  23801  fta1  23812  aalioulem2  23837  aalioulem3  23838  ulmuni  23895  ulmbdd  23901  ulmdvlem3  23905  mtest  23907  abelthlem8  23942  pilem3  23956  efopn  24149  cxpmul2z  24182  cxpcn3lem  24233  jensen  24460  lgambdd  24508  lgamucov  24509  isppw2  24586  sqf11  24610  mersenne  24697  dchrelbas3  24708  dchrptlem1  24734  dchrpt  24737  lgsval2lem  24777  lgsdchrval  24824  lgsquad3  24857  2sqb  24902  pntrsumbnd2  25001  pntpbnd  25022  pntibnd  25027  istrkgc  25098  istrkgb  25099  tglowdim1i  25141  tgbtwndiff  25146  tgifscgr  25149  iscgrglt  25155  tgcgrxfr  25159  lnext  25208  tgbtwnconn1lem3  25215  tgbtwnconn1  25216  legval  25225  legov  25226  legov2  25227  legtrd  25230  legtri3  25231  legso  25240  hlcgrex  25257  hlcgreu  25259  tglnne  25269  tglndim0  25270  tglineeltr  25272  tglinethru  25277  tglnne0  25281  tglnpt2  25282  colline  25290  tglowdim2l  25291  tglowdim2ln  25292  mirreu3  25295  miriso  25311  midexlem  25333  isperp  25353  perpcom  25354  perpneq  25355  isperp2  25356  footex  25359  colperpexlem3  25370  opphllem  25373  midex  25375  oppne3  25381  opptgdim2  25383  opphllem2  25386  opphllem3  25387  opphllem5  25389  opphllem6  25390  opphl  25392  outpasch  25393  lnopp2hpgb  25401  colopp  25407  lmieu  25422  trgcopy  25442  trgcopyeu  25444  iscgra1  25448  cgrane1  25450  cgrane2  25451  cgrane3  25452  cgrahl1  25454  cgrahl2  25455  cgracgr  25456  cgraswap  25458  cgracom  25460  cgratr  25461  cgrabtwn  25463  cgrahl  25464  dfcgra2  25467  sacgr  25468  acopyeu  25471  inaghl  25477  cgrg3col4  25480  f1otrg  25497  f1otrge  25498  axsegcon  25553  axeuclidlem  25588  axcontlem2  25591  usgra1  25696  usgrares1  25733  nbgraf1olem5  25768  pthdepisspth  25898  clwwlkf1  26118  clwwlknscsh  26141  el2spthonot  26191  usg2wotspth  26205  iseupa  26286  eupath2  26301  frgrancvvdeqlem9  26362  friendshipgt3  26442  smcnlem  26765  0lno  26863  ubthlem1  26944  ubthlem3  26946  chocunii  27378  occl  27381  5oalem1  27731  3oalem2  27740  nmopub2tALT  27986  nmfnleub2  28003  lnconi  28110  kbass5  28197  mdslmd1lem1  28402  mdslmd1lem2  28403  cdj1i  28510  disjabrex  28611  disjabrexf  28612  acunirnmpt  28675  acunirnmpt2  28676  acunirnmpt2f  28677  aciunf1lem  28678  fgreu  28688  xrge0infss  28749  xrofsup  28757  2sqmo  28814  ressprs  28820  xrge0addgt0  28856  submarchi  28905  isarchi3  28906  archiabllem1  28912  archiabllem2a  28913  gsumle  28944  suborng  28980  isarchiofld  28982  psgnfzto1stlem  29015  fzto1st1  29017  mdetpmtr1  29051  fimaproj  29062  txomap  29063  qtophaus  29065  cmpcref  29079  pstmxmet  29102  sqsscirc1  29116  ordtrest2NEWlem  29130  ordtconlem1  29132  pnfneige0  29159  lmxrge0  29160  lmdvg  29161  qqhval2  29188  esumcst  29286  esumrnmpt2  29291  esumfsup  29293  esumcvg  29309  esum2d  29316  esumiun  29317  sigaclfu2  29345  insiga  29361  ldsysgenld  29384  ldgenpisyslem1  29387  fiunelros  29398  measinb  29445  imambfm  29485  oms0  29520  omssubadd  29523  carsgclctunlem3  29543  eulerpartlemgvv  29599  dstrvprob  29694  sgnsub  29767  signstfvneq0  29809  afsval  29836  derangenlem  30241  sconpi1  30309  cvmsss2  30344  cvmopnlem  30348  cvmlift3lem7  30395  msrval  30523  ifscgr  31155  cgrxfr  31166  btwnconn1lem13  31210  outsideofeu  31242  neibastop2lem  31359  matunitlindflem1  32399  matunitlindflem2  32400  poimirlem14  32417  poimirlem22  32425  poimirlem29  32432  broucube  32437  heicant  32438  mblfinlem1  32440  itg2addnclem  32455  ftc1cnnc  32478  ftc1anclem7  32485  sstotbnd2  32567  equivtotbnd  32571  isbnd3  32577  ssbnd  32581  totbndbnd  32582  cntotbnd  32589  heibor1lem  32602  rrncmslem  32625  lssats  33141  lsat0cv  33162  lkrlss  33224  lfl1dim  33250  lfl1dim2N  33251  lkrpssN  33292  hlhgt2  33517  3dim2  33596  2dim  33598  lplncvrlvol  33744  paddasslem11  33958  pmapjat1  33981  2polssN  34043  pclfinclN  34078  pexmidlem8N  34105  lhpexle1lem  34135  4atex  34204  ltrnid  34263  trlator0  34300  cdlemg2cex  34721  tendodi1  34914  tendodi2  34915  diblss  35301  dihopelvalcpre  35379  dihatexv  35469  mapdval4N  35763  mzpindd  36151  mzpsubst  36153  mzpcompact2lem  36156  eldioph2b  36168  irrapxlem3  36230  irrapxlem5  36232  pellex  36241  pell1234qrdich  36267  pell14qrexpcl  36273  congabseq  36383  jm2.26a  36409  jm2.26lem3  36410  rmydioph  36423  lnrfg  36532  hbt  36543  rfovcnvf1od  37142  clsk3nimkb  37182  ntrneiiso  37233  ntrneikb  37236  ntrneixb  37237  ntrneik3  37238  ntrneix3  37239  ntrneik13  37240  ntrneix13  37241  4an4132  37550  iunconlem2  38017  fnchoice  38035  cncmpmax  38038  ssinc  38116  ssdec  38117  disjf1  38188  supxrge  38319  suplesup  38320  infxr  38348  infleinf  38353  climrec  38494  climsuse  38499  islptre  38510  addlimc  38539  0ellimcdiv  38540  icccncfext  38597  cncfiooicclem1  38603  fperdvper  38632  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvmptfprodlem  38658  dvmptfprod  38659  dvnprodlem2  38661  stoweidlem7  38724  stoweidlem34  38751  stoweidlem52  38769  stoweidlem60  38777  wallispilem3  38784  fourierdlem34  38858  fourierdlem38  38862  fourierdlem39  38863  fourierdlem48  38871  fourierdlem50  38873  fourierdlem51  38874  fourierdlem73  38896  fourierdlem76  38899  fourierdlem77  38900  fourierdlem80  38903  fourierdlem87  38910  fourierdlem103  38926  fourierdlem104  38927  etransclem32  38983  etransclem33  38984  sge0f1o  39099  sge0pr  39111  sge0isum  39144  iundjiun  39177  meaiininclem  39200  pimdecfgtioo  39428  pimincfltioo  39429  preimageiingt  39431  preimaleiinlt  39432  smflimlem2  39482  smflimlem4  39484  smfmullem3  39502  bgoldbtbndlem2  40047  bgoldbtbndlem3  40048  bgoldbtbnd  40050  upgr1eopALT  40364  usgr1eop  40498  pthdepissPth  40963  clwwlksf1  41246  clwwlksnscsh  41269  2pthfrgr  41476  n4cyclfrgr  41483  av-friendshipgt3  41574  mgmhmeql  41615  isrng  41688  2zlidl  41746  lindslinindsimp2  42068  snlindsntor  42076  lincresunit2  42083  islindeps2  42088
  Copyright terms: Public domain W3C validator