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

Theorem simpl1 1084
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 1081 . 2 ((𝜑𝜓𝜒) → 𝜑)
21adantr 480 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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  df-an 385  df-3an 1056
This theorem is referenced by:  simpll1  1120  simprl1  1126  simp1l1  1174  simp2l1  1180  simp3l1  1186  3anandirs  1475  rspc3ev  3357  f1prex  6579  cocan1  6586  weniso  6644  smogt  7509  smorndom  7510  omeulem1  7707  nnmord  7757  nnmword  7758  difsnen  8083  enfixsn  8110  mapunen  8170  ac6sfi  8245  fipreima  8313  elfiun  8377  ordiso2  8461  wemaplem2  8493  wemapso  8497  en2eqpr  8868  indcardi  8902  fodomfi2  8921  iunfictbso  8975  infmap2  9078  cofsmo  9129  cfsmolem  9130  coftr  9133  fin23lem11  9177  fincssdom  9183  fin23lem26  9185  isf32lem9  9221  ac6num  9339  gchdomtri  9489  gchpwdom  9530  winainflem  9553  tskuni  9643  gruima  9662  gruf  9671  grudomon  9677  elnpi  9848  distrlem4pr  9886  prlem934  9893  addcan  10258  addcan2  10259  divmulass  10746  divmulasscom  10747  ltmul1a  10910  suprleub  11027  supmul1  11030  suprzcl  11495  uzsupss  11818  xleadd1a  12121  xlesubadd  12131  xmulasslem3  12154  xlemul2a  12157  xadddilem  12162  xadddi2  12165  ixxun  12229  icoshftf1o  12333  snunioc  12338  lincmb01cmp  12353  iccf1o  12354  nn0p1elfzo  12550  fzofzim  12554  ltexp2a  12952  leexp2  12955  ltexp2r  12957  exple1  12960  expnlbnd2  13035  fun2dmnop0  13314  ccatass  13406  ccat2s1fvw  13460  swrdswrdlem  13505  ccatopth  13516  cshimadifsn  13621  cshimadifsn0  13622  cshco  13628  repsco  13631  s2f1o  13707  limsupgre  14256  addcn2  14368  mulcn2  14370  ntrivcvgmul  14678  binomrisefac  14817  dvdsmodexp  15035  dvdsadd2b  15075  dvdsmod  15097  oexpneg  15116  sadass  15240  gcdass  15311  rplpwr  15323  rppwr  15324  lcmfunsnlem1  15397  coprmdvds2  15415  rpmulgcd2  15417  qredeq  15418  rpdvds  15421  cncongr2  15429  rpexp  15479  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  modprmn0modprm0  15559  coprimeprodsq2  15561  pythagtriplem3  15570  pcdvdsb  15620  pcgcd1  15628  qexpz  15652  pockthg  15657  vdwnnlem1  15746  0ram  15771  ramz2  15775  lubss  17168  lubun  17170  clatleglb  17173  clatglbss  17174  mrelatglb  17231  isnsgrp  17335  issubmnd  17365  ress0g  17366  gsumccat  17425  frmdss2  17447  mulgneg  17607  mulgdirlem  17619  submmulg  17633  subgmulg  17655  nmzsubg  17682  ghmmulg  17719  gsmsymgreqlem1  17896  pmtrfb  17931  psgnunilem4  17963  odmodnn0  18005  odnncl  18010  odmod  18011  odmulgid  18017  odmulgeq  18020  odf1o1  18033  odf1o2  18034  odngen  18038  gexdvdsi  18044  pgpfi1  18056  odcau  18065  subgslw  18077  fislw  18086  lsmssv  18104  lsmless1x  18105  lsmless2x  18106  lsmsubm  18114  lsmmod  18134  lsmmod2  18135  efgred  18207  cntzcmn  18291  ghmplusg  18295  odadd1  18297  odadd2  18298  odadd  18299  lsmcomx  18305  gsumconst  18380  srg1zr  18575  ring1eq0  18636  mulgass2  18647  isabvd  18868  rmodislmodlem  18978  rmodislmod  18979  lssintcl  19012  0lmhm  19088  lmhmvsca  19093  reslmhm2b  19102  pwssplit1  19107  pwssplit3  19109  lspfixed  19176  lspsnat  19193  lidldvgen  19303  issubassa  19372  evlsval2  19568  psrplusgpropd  19654  coe1subfv  19684  coe1mul2  19687  xrsdsreclblem  19840  regsumsupp  20016  obselocv  20120  uvcresum  20180  frlmsslsp  20183  frlmup4  20188  lindff1  20207  f1lindf  20209  lsslindf  20217  islindf4  20225  lbslcic  20228  mhmvlin  20251  mpt2matmul  20300  mamutpos  20312  scmatscmide  20361  mavmulsolcl  20405  marrepcl  20418  mdetdiag  20453  mdetunilem1  20466  mdetunilem3  20468  mdetunilem7  20472  mdetunilem9  20474  mdetmul  20477  slesolinvbi  20535  m2pmfzmap  20600  pmatcollpwlem  20633  pmatcollpw  20634  mp2pm2mplem4  20662  chpdmatlem3  20693  chfacfisfcpmat  20708  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmidpmatlem2  20724  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  riinopn  20761  neiint  20956  topssnei  20976  restntr  21034  iscnp4  21115  cnconst2  21135  cnrest2  21138  cnprest2  21142  cnpdis  21145  cnt0  21198  cnt1  21202  cnhaus  21206  ordthauslem  21235  cncmp  21243  fiuncmp  21255  sscmp  21256  hauscmp  21258  cnconn  21273  unconn  21280  nlly2i  21327  llynlly  21328  nllyidm  21340  finlocfin  21371  ptrescn  21490  xkococnlem  21510  qtoptop2  21550  qtopss  21566  kqfvima  21581  r0cld  21589  ordthmeolem  21652  fbssint  21689  fmf  21796  fmss  21797  elfm  21798  rnelfmlem  21803  rnelfm  21804  fmco  21812  flimss2  21823  flimss1  21824  flimrest  21834  flftg  21847  cnpflf2  21851  cnpflf  21852  flfcnp  21855  supnfcls  21871  fclsss1  21873  fclsss2  21874  fcfnei  21886  fcfelbas  21887  cnpfcfi  21891  subgntr  21957  opnsubg  21958  cldsubg  21961  ghmcnp  21965  utop2nei  22101  neipcfilu  22147  bldisj  22250  blgt0  22251  bl2in  22252  blss2ps  22255  blss2  22256  blssps  22276  blss  22277  xmetresbl  22289  lpbl  22355  blcld  22357  stdbdbl  22369  metcnp3  22392  metcnp2  22394  txmetcnp  22399  blval2  22414  nmoix  22580  nmoeq0  22587  icoopnst  22785  iocopnst  22786  xrhmeo  22792  nmhmcn  22966  cphsqrtcl2  23032  cphsqrtcl3  23033  cfil3i  23113  caublcls  23153  bcthlem5  23171  cmetcusp1  23195  rrxcph  23226  pjth  23256  ovoliunlem2  23317  volun  23359  volsup2  23419  mbfimaopn2  23469  iblconst  23629  itgconst  23630  dvcnp2  23728  dvcn  23729  deg1mul3le  23921  deg1tmle  23922  dvdsq1p  23965  ig1peu  23976  ig1pdvds  23981  coeid3  24041  dgrmulc  24072  efcvx  24248  tanord  24329  logdivlti  24411  logccv  24454  recxpcl  24466  cxpeq  24543  ang180  24589  isosctrlem2  24594  cxp2lim  24748  amgm  24762  muval1  24904  dvdssqf  24909  mumullem2  24951  mumul  24952  bcmono  25047  lgsfcl2  25073  lgsdilem  25094  lgsdirprm  25101  lgsdir  25102  lgsdi  25104  lgsne0  25105  padicabv  25364  brbtwn2  25830  colinearalglem1  25831  colinearalg  25835  axcgrtr  25840  axsegconlem8  25849  axsegconlem9  25850  axsegconlem10  25851  axcontlem8  25896  axcontlem10  25898  vtxdlfuhgr1v  26431  umgr2wlk  26914  erclwwlksym  26978  clwwlkfo  27013  clwwlkext2edg  27020  erclwwlknsym  27034  clwlksf1clwwlklem  27055  clwwlknon1  27072  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  numclwwlk5  27375  frgrregord13  27383  nvmul0or  27633  ipval2lem2  27687  lnomul  27743  shless  28346  shlej1  28347  pjspansn  28564  hoadddi  28790  kbmul  28942  homco2  28964  kbass2  29104  eliccelico  29667  elicoelioo  29668  iocinioc2  29669  iocinif  29671  xrge0adddir  29820  xrge0npcan  29822  archiabl  29880  ress1r  29917  rhmdvdsr  29946  pstmfval  30067  fmcncfil  30105  zrhnm  30141  qqhnm  30162  measvunilem  30403  volfiniune  30421  dya2iocnrect  30471  sibfinima  30529  probun  30609  probinc  30611  cndprob01  30625  bnj517  31081  bnj594  31108  pconnpi1  31345  cvmsss2  31382  mrsubcv  31533  msubvrs  31583  dvdspw  31762  br6  31773  br4  31774  frpomin  31863  frrlem4  31908  nosep1o  31957  nosepssdm  31961  nolt02olem  31969  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  nosupbnd2  31987  noetalem2  31989  cgrcomim  32221  cgrtriv  32234  cgrextend  32240  segconeq  32242  btwntriv2  32244  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  trisegint  32260  cgrsub  32277  cgrxfr  32287  btwnxfr  32288  lineext  32308  btwnconn1lem13  32331  btwnconn1lem14  32332  btwnconn3  32335  segcon2  32337  brsegle  32340  brsegle2  32341  segletr  32346  segleantisym  32347  seglelin  32348  outsideofeu  32363  lineunray  32379  lineelsb2  32380  ivthALT  32455  lindsenlbs  33534  areacirc  33635  cocanfo  33642  upixp  33654  ismtyima  33732  rrndstprj2  33760  zerdivemp1x  33876  lsatfixedN  34614  lssat  34621  eqlkr  34704  eqlkr2  34705  lkrlsp  34707  lshpkrlem4  34718  opposet  34786  cvrcon3b  34882  cvrcmp  34888  atlen0  34915  atnle  34922  atlatmstc  34924  cvlatexch3  34943  cvlsupr2  34948  hlsupr2  34991  hlrelat2  35007  cvrexchlem  35023  lnnat  35031  atcvrj2b  35036  atle  35040  atexchcvrN  35044  atbtwn  35050  athgt  35060  3dimlem3  35065  3dim1  35071  1cvratlt  35078  1cvrjat  35079  ps-1  35081  ps-2  35082  3atlem3  35089  3atlem5  35091  3atlem7  35093  llni  35112  llni2  35116  atcvrlln2  35123  llnexatN  35125  llncmp  35126  2llnmat  35128  2at0mat0  35129  lplni  35136  lplnnle2at  35145  2atnelpln  35148  lplnllnneN  35160  llncvrlpln2  35161  2lplnmN  35163  2llnmj  35164  lplncmp  35166  lplnexatN  35167  lplnexllnN  35168  2llnm3N  35173  lvoli  35179  lvoli3  35181  islvol2aN  35196  4atlem0a  35197  4atlem3  35200  4atlem3a  35201  4atlem4a  35203  4atlem4b  35204  4atlem4c  35205  4atlem4d  35206  4atlem10b  35209  4atlem11  35213  4atlem12  35216  lplncvrlvol2  35219  lvolcmp  35221  2lplnmj  35226  islinei  35344  pmapglbx  35373  linepmap  35379  lneq2at  35382  lnjatN  35384  lncvrat  35386  lncmp  35387  2llnma3r  35392  elpaddatriN  35407  elpaddat  35408  paddcom  35417  paddss1  35421  paddss2  35422  paddss12  35423  paddasslem6  35429  paddasslem7  35430  paddasslem8  35431  paddasslem9  35432  paddasslem15  35438  pmodlem2  35451  pmodl42N  35455  pmapjoin  35456  llnmod1i2  35464  2polcon4bN  35522  polcon2bN  35524  poml4N  35557  poml6N  35559  osumcllem1N  35560  osumcllem2N  35561  osumcllem11N  35570  osumclN  35571  pmapojoinN  35572  pexmidlem2N  35575  pexmidlem3N  35576  pexmidlem4N  35577  pexmidlem6N  35579  pexmidlem7N  35580  pl42lem2N  35584  pl42lem3N  35585  pl42lem4N  35586  pl42N  35587  lhpexle2lem  35613  lhpexle3lem  35615  lhpexle3  35616  lhpmcvr3  35629  lhp2at0nle  35639  lhprelat3N  35644  4atex  35680  4atex2  35681  lauteq  35699  lautco  35701  ltrncoidN  35732  ltrneq2  35752  ltrnnidn  35779  ltrnideq  35780  trlnid  35784  ltrnatlw  35788  trlnle  35791  trlval3  35792  trlval4  35793  cdlemc  35802  cdlemd5  35807  cdlemd9  35811  ltrneq3  35813  cdleme0moN  35830  cdleme20  35929  cdleme21j  35941  cdleme21  35942  cdleme27cl  35971  cdlemefrs29bpre0  36001  cdlemefs27cl  36018  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme32d  36049  cdleme32f  36051  cdleme32le  36052  cdleme35h2  36062  cdleme38n  36069  cdleme40m  36072  cdleme41snaw  36081  cdleme42ke  36090  cdleme17d3  36101  cdleme48fvg  36105  cdlemeg46fvcl  36111  cdlemeg46fgN  36139  cdleme48gfv1  36141  cdleme48fgv  36143  cdleme50trn3  36158  trlord  36174  ltrniotavalbN  36189  cdlemb3  36211  cdlemg6c  36225  cdlemg6  36228  cdlemg7N  36231  cdlemg8c  36234  cdlemg8  36236  cdlemg11a  36242  cdlemg11b  36247  cdlemg12e  36252  cdlemg15a  36260  cdlemg15  36261  cdlemg16  36262  cdlemg16z  36264  cdlemg16zz  36265  cdlemg17dN  36268  cdlemg18a  36283  cdlemg20  36290  cdlemg22  36292  cdlemg24  36293  cdlemg37  36294  cdlemg31d  36305  cdlemg29  36310  cdlemg33b  36312  cdlemg33  36316  cdlemg38  36320  cdlemg39  36321  cdlemg40  36322  trlco  36332  trlcone  36333  cdlemg42  36334  cdlemg44b  36337  ltrncom  36343  trljco  36345  tendococl  36377  tendoplcl  36386  tendoplcom  36387  cdlemj2  36427  cdlemj3  36428  tendoid0  36430  tendoconid  36434  tendotr  36435  cdlemk25-3  36509  cdlemk26b-3  36510  cdlemk34  36515  cdlemk36  36518  cdlemk38  36520  cdlemkid4  36539  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk19x  36548  cdlemk53  36562  cdlemk55  36566  cdlemk55u  36571  cdlemk39u  36573  cdlemk19u  36575  cdlemk56  36576  tendoex  36580  cdleml3N  36583  cdleml5N  36585  tendospcanN  36629  cdlemm10N  36724  cdlemn11pre  36816  dihord2pre  36831  dihvalcqpre  36841  dihopelvalcpre  36854  dihord6apre  36862  dihord5b  36865  dihord5apre  36868  dihord  36870  dihmeetlem1N  36896  dihglblem5apreN  36897  dihglblem3N  36901  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetbN  36909  dihmeetlem4preN  36912  dihmeetlem5  36914  dihmeetlem7N  36916  dihmeetlem10N  36922  dihmeetlem11N  36923  dihmeetlem12N  36924  dihmeetlem13N  36925  dihmeetlem15N  36927  dihmeetlem16N  36928  dihmeetlem17N  36929  dihmeetlem18N  36930  dihmeetlem19N  36931  dihmeetALTN  36933  dih1dimatlem0  36934  dihlspsnssN  36938  dihlspsnat  36939  mapdh8ad  37385  hdmap14lem14  37490  hgmapvvlem3  37534  mzprename  37629  eldioph2lem1  37640  lzunuz  37648  rencldnfi  37702  pellexlem2  37711  infmrgelbi  37759  pellfundglb  37766  pellfund14gap  37768  qirropth  37790  rmxycomplete  37799  congadd  37850  acongeq  37867  jm2.19  37877  jm2.23  37880  jm2.20nn  37881  jm2.27  37892  jm3.1  37904  aomclem6  37946  lnmepi  37972  lmhmfgsplit  37973  lmhmlnmsplit  37974  pwssplit4  37976  hbtlem2  38011  hbtlem5  38015  dgraa0p  38036  proot1hash  38095  iocunico  38113  relexpxpmin  38326  brtrclfv2  38336  ntrclsiso  38682  ntrclskb  38684  ntrclsk3  38685  k0004lem3  38764  suprnmpt  39669  wessf1ornlem  39685  projf1o  39700  snunioo2  40049  snunioo1  40056  iccintsng  40067  lptre2pt  40190  limcleqr  40194  fnlimfvre  40224  limsupgtlem  40327  volioc  40506  iblspltprt  40507  stoweidlem19  40554  stoweidlem20  40555  stoweidlem22  40557  stoweidlem28  40563  stoweidlem34  40569  stoweidlem44  40579  stoweidlem60  40595  wallispilem3  40602  fourierdlem41  40683  fourierdlem42  40684  fourierdlem49  40690  fourierdlem51  40692  fourierdlem54  40695  fourierdlem74  40715  fourierdlem97  40738  caratheodorylem2  41062  ovnsubaddlem2  41106  hspmbllem2  41162  smflimmpt  41337  smflimsupmpt  41356  smfliminfmpt  41359  fzopredsuc  41658  fzoopth  41662  iccpartigtl  41684  repswpfx  41761  lighneal  41853  oexpnegALTV  41913  oexpnegnz  41914  tgblthelfgott  42028  tgblthelfgottOLD  42034  lidldomn1  42246  ofaddmndmap  42447  lincdifsn  42538  lincellss  42540  lincresunit3lem3  42588  islindeps2  42597  lindssnlvec  42600  fdivmptf  42660  refdivmptf  42661
  Copyright terms: Public domain W3C validator