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

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

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 1055 . 2 ((𝜑𝜓𝜒) → 𝜒)
21adantr 479 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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  df-3an 1032
This theorem is referenced by:  simpll3  1094  simprl3  1100  simp1l3  1148  simp2l3  1154  simp3l3  1160  3anandirs  1426  f1prex  6413  fcofo  6417  soisores  6451  weniso  6478  knatar  6481  ofmpteq  6787  smorndom  7325  nnmord  7572  nnmword  7573  difsnen  7900  mapunen  7987  ac6sfi  8062  fipreima  8128  wemaplem2  8308  wemapso2lem  8313  en2eqpr  8686  indcardi  8720  acndom  8730  fodomfi2  8739  infmap2  8896  cflim2  8941  coftr  8951  infpssrlem4  8984  fin23lem11  8995  fincssdom  9001  isf32lem9  9039  fin1a2lem9  9086  gchpwdom  9344  gruima  9476  prpssnq  9664  distrlem4pr  9700  dedekind  10047  addcan  10067  addcan2  10068  divmulass  10553  supmul1  10835  uzsupss  11608  xaddass  11904  xleadd1a  11908  xlesubadd  11918  xmulasslem3  11941  xmulass  11942  xadddilem  11949  xadddi  11950  ixxun  12014  icoshftf1o  12118  snunioc  12123  difelfzle  12272  fzo1fzo0n0  12337  ssfzoulel  12379  modmuladd  12525  modifeq2int  12545  modaddmulmod  12550  modsubdir  12552  ltexp2a  12725  leexp2  12728  ltexp2r  12730  exple1  12733  expnlbnd2  12808  mulsubdivbinom2  12859  hashtpg  13067  ccatass  13166  ccatopth  13264  swrdccatin12lem2a  13278  swrdccat3  13285  cshinj  13350  s2f1o  13453  limsupgre  14002  addcn2  14114  mulcn2  14116  binomrisefac  14554  bpolydif  14567  modmulconst  14793  dvdsmod  14830  sadass  14973  gcdass  15044  rplpwr  15056  rppwr  15057  rpmulgcd2  15150  rpdvds  15154  rpexp  15212  prmdiveq  15271  hashgcdlem  15273  coprimeprodsq  15293  coprimeprodsq2  15294  pythagtriplem3  15303  pcdvdsb  15353  pcgcd1  15361  dvdsprmpweq  15368  pcbc  15384  0ram  15504  ramz2  15508  ramub1lem1  15510  setsstruct  15669  mremre  16029  mrieqv2d  16064  lubun  16888  isnsgrp  17053  issubmnd  17083  gsumccat  17143  frmdss2  17165  sgrp2rid2ex  17179  mulgnn0p1  17317  mulgnnsubcl  17318  mulgneg  17325  mulgdirlem  17337  nmzsubg  17400  ghmmulg  17437  pmtrfv  17637  pmtrmvd  17641  pmtrfb  17650  odmodnn0  17724  oddvdsnn0  17728  odnncl  17729  odmod  17730  oddvds  17731  odeq  17734  odmulgid  17736  odmulg  17738  odmulgeq  17739  odbezout  17740  odf1o1  17752  odf1o2  17753  odngen  17757  odcau  17784  pgpssslw  17794  fislw  17805  lsmless1x  17824  lsmless2x  17825  lsmsubm  17833  lsmmod  17853  lsmmod2  17854  efgsfo  17917  cntzcmn  18010  odadd1  18016  odadd2  18017  odadd  18018  lsmcomx  18024  prdscmnd  18029  gsumconst  18099  ring1eq0  18355  cntzsubr  18577  isabvd  18585  lspss  18747  0lmhm  18803  reslmhm2  18816  pwssplit0  18821  pwssplit1  18822  lbspss  18845  lspfixed  18891  lsmcv  18904  lspsnat  18908  issubassa  19087  aspss  19095  coe1subfv  19399  coe1tm  19406  xrsdsreclblem  19553  obselocv  19829  frlmsplit2  19869  frlmsslss2  19871  frlmup4  19897  lindff1  19916  lsslindf  19926  lsslinds  19927  islindf4  19934  mpt2matmul  20009  mamutpos  20021  submaval  20144  mdetdiag  20162  mdetunilem1  20175  mdetunilem3  20177  mdetunilem9  20183  mdetmul  20186  maducoeval2  20203  madurid  20207  minmar1val  20211  cramer  20254  cpmatel2  20275  m2cpm  20303  decpmatmul  20334  pmatcollpw1lem2  20337  pmatcollpw1  20338  pmatcollpw2lem  20339  pm2mpcl  20359  mply1topmatcl  20367  mp2pm2mplem2  20369  mp2pm2mplem4  20371  pm2mpghmlem2  20374  pm2mpghmlem1  20375  cayhamlem2  20446  neiint  20656  topssnei  20676  cnrest2  20838  cnprest2  20842  cnt0  20898  cnt1  20902  cnhaus  20906  cncmp  20943  fiuncmp  20955  sscmp  20956  hauscmp  20958  cnconn  20973  uncon  20980  comppfsc  21083  kgen2ss  21106  ptpjopn  21163  ptrescn  21190  qtopss  21266  kqfvima  21281  r0cld  21289  cmphaushmeo  21351  fbssint  21390  fbasrn  21436  filuni  21437  ufilmax  21459  fin1aufil  21484  fmf  21497  fmss  21498  rnelfmlem  21504  rnelfm  21505  fmufil  21511  fmco  21513  flimss2  21524  flimss1  21525  flimrest  21535  cnpflf2  21552  cnpflf  21553  flfcnp  21556  lmflf  21557  supnfcls  21572  fclsss1  21574  fclsss2  21575  cnpfcfi  21592  subgntr  21658  opnsubg  21659  cldsubg  21662  ustuqtop1  21793  ucncn  21837  bldisj  21950  blgt0  21951  bl2in  21952  blss2ps  21955  blss2  21956  xbln0  21966  blssps  21976  blss  21977  lpbl  22055  blcld  22057  blcls  22058  stdbdmopn  22070  metcnp2  22094  txmetcnp  22099  blval2  22114  restmetu  22122  nmoix  22271  nmoi2  22272  nmoeq0  22278  nmotri  22281  metdsge  22387  metds0  22388  metdseq0  22392  icoopnst  22473  iccpnfhmeo  22479  xrhmeo  22480  nmhmcn  22655  cphsqrtcl2  22714  cphsqrtcl3  22715  fmcfil  22792  bcthlem5  22846  cmetcusp1  22870  pjth  22931  ovolunnul  22988  volun  23033  voliunlem2  23039  itg2const  23226  iblconst  23303  itgconst  23304  limcvallem  23354  dvcnp2  23402  dvcn  23403  deg1mul3le  23593  deg1tmle  23594  ig1pdvds  23653  coe11  23726  dgrmulc  23744  dvply1  23756  aaliou2  23812  efcvx  23920  tanord  24001  logdivlti  24083  logccv  24122  recxpcl  24134  cxplea  24155  cxple2a  24158  ang180  24257  isosctrlem2  24262  cxp2lim  24416  amgm  24430  muval1  24572  dvdssqf  24577  mumullem2  24619  bcmono  24715  lgsneg  24759  lgsmod  24761  lgsdirprm  24769  lgsdir  24770  lgsdi  24772  brbtwn2  25499  colinearalglem1  25500  colinearalg  25504  axcgrtr  25509  axcontlem2  25559  cyclispthon  25923  clwwlknprop  26062  clwwlknimp  26066  vdgrfif  26188  4cyclusnfrgra  26308  nvmul0or  26673  shless  27404  shlej1  27405  pjspansn  27622  kbmul  28000  homco2  28022  kbass2  28162  padct  28687  eliccelico  28731  elicoelioo  28732  iocinioc2  28733  difioo  28736  xrge0npcan  28827  isarchi2  28872  archiabl  28885  mdetlap1  29022  pstmfval  29069  fmcncfil  29107  zrhnm  29143  qqhnm  29164  nexple  29201  volfiniune  29422  omsmeas  29514  eulerpartlemb  29559  probinc  29612  cndprob01  29626  signswmnd  29762  cvmsss2  30312  dvdspw  30691  funsseq  30714  sltres  30863  cgrtriv  31081  5segofs  31085  btwntriv2  31091  btwnxfr  31135  segcon2  31184  brsegle2  31188  seglelin  31195  outsideofeu  31210  lindsenlbs  32373  mblfinlem2  32416  blbnd  32555  rrndstprj2  32599  zerdivemp1x  32715  lsmsat  33112  lsatfixedN  33113  lssat  33120  lkrlsp  33206  lshpkrlem4  33217  cvrcon3b  33381  leat3  33399  atlen0  33414  atnle  33421  atlatmstc  33423  atlatle  33424  cvlcvr1  33443  cvlsupr2  33447  hlsupr2  33490  hlrelat2  33506  cvrexchlem  33522  cvratlem  33524  lnnat  33530  atexchcvrN  33543  1cvratlt  33577  1cvrjat  33578  3atlem3  33588  3atlem7  33592  llni2  33615  atcvrlln2  33622  llnexatN  33624  llncmp  33625  2llnmat  33627  2at0mat0  33628  2atnelpln  33647  llncvrlpln2  33660  2lplnmN  33662  2llnmj  33663  lplncmp  33665  lplnexatN  33666  2llnjaN  33669  lvoli3  33680  islvol2aN  33695  4atlem3a  33700  4atlem4a  33702  4atlem4b  33703  4atlem11  33712  4atlem12  33715  lplncvrlvol2  33718  lvolcmp  33720  2lplnmj  33725  islinei  33843  linepmap  33878  lneq2at  33881  2llnma3r  33891  elpaddn0  33903  elpaddatriN  33906  elpaddat  33907  paddcom  33916  paddss1  33920  paddss2  33921  paddasslem6  33928  paddasslem7  33929  paddasslem10  33932  paddasslem15  33937  pmodlem2  33950  pmodl42N  33954  pmapjoin  33955  atmod1i1m  33961  llnmod1i2  33963  llnexchb2lem  33971  polcon2bN  34023  pclfinclN  34053  poml4N  34056  poml6N  34058  osumcllem11N  34069  osumclN  34070  pmapojoinN  34071  pexmidlem2N  34074  pexmidlem3N  34075  pexmidlem4N  34076  pexmidlem6N  34078  pexmidlem7N  34079  pl42lem2N  34083  pl42lem3N  34084  pl42lem4N  34085  pl42N  34086  lhpexle3lem  34114  lhpmcvr3  34128  lhp2at0nle  34138  lhprelat3N  34143  lauteq  34198  lautco  34200  ltrncoidN  34231  ltrneq2  34251  ltrnnidn  34278  ltrnideq  34279  trlnle  34290  cdlemc  34301  cdlemd4  34305  cdlemd5  34306  cdlemd9  34310  cdlemd  34311  ltrneq3  34312  cdlemefrs29pre00  34500  cdlemefrs29cpre1  34503  cdlemefrs29clN  34504  cdlemefrs32fva  34505  cdlemefr29exN  34507  cdlemefr27cl  34508  cdlemefs27cl  34518  cdlemefs32sn1aw  34519  cdleme32fva  34542  cdleme32d  34549  cdleme32f  34551  cdleme32le  34552  cdleme40n  34573  cdleme41snaw  34581  cdleme17d3  34601  cdleme48fvg  34605  cdlemeg46fvcl  34611  cdlemeg46fgN  34639  cdleme48fgv  34643  ltrniotavalbN  34689  cdlemb3  34711  cdlemg15  34761  cdlemg17dN  34768  trlco  34832  cdlemg44b  34837  ltrncom  34843  trljco  34845  tendococl  34877  tendoplcl  34886  tendoplcom  34887  tendotr  34935  cdlemk36  35018  cdlemk35s-id  35043  cdlemk39s-id  35045  cdlemk19x  35048  cdlemk53b  35061  cdlemk55  35066  cdlemk35u  35069  cdlemk55u  35071  cdlemk39u  35073  cdlemk19u  35075  cdlemk56  35076  tendoex  35080  cdleml5N  35085  dihord2pre  35331  dihord6apre  35362  dihord5b  35365  dihord5apre  35368  dihord  35370  dihmeetlem1N  35396  dihmeetlem2N  35405  dihglbcpreN  35406  dihmeetbN  35409  dihmeetlem4preN  35412  dihmeetlem5  35414  dihmeetlem6  35415  dihmeetlem7N  35416  dihmeetlem10N  35422  dihmeetlem11N  35423  dihmeetlem12N  35424  dihmeetlem13N  35425  dihmeetlem15N  35427  dihmeetlem17N  35429  dihmeetlem18N  35430  dihmeetlem19N  35431  dihmeetALTN  35433  dih1dimatlem0  35434  dihlspsnssN  35438  dvh3dim2  35554  mzpsubst  36128  diophrw  36139  eldioph2lem1  36140  rencldnfi  36202  pellexlem2  36211  pellqrexplicit  36258  infmrgelbi  36259  rmxycomplete  36299  congadd  36350  acongeq  36367  jm2.19  36377  jm2.22  36379  jm2.20nn  36381  jm2.25lem1  36382  jm2.27  36392  jm3.1  36404  lmhmlnmsplit  36474  pwssplit4  36476  hbtlem2  36512  dgraa0p  36537  idomrootle  36591  proot1hash  36596  iocunico  36614  relexpxpmin  36827  brtrclfv2  36837  ntrclsk3  37187  suprnmpt  38149  wessf1ornlem  38165  choicefi  38186  supxrgere  38290  supxrgelem  38294  supxrge  38295  infleinflem2  38328  snunioo1  38385  iccintsng  38396  fmul01  38447  lptre2pt  38507  0ellimcdiv  38516  fnlimfvre  38541  ibliccsinexp  38642  iblioosinexp  38644  volioc  38664  iblspltprt  38665  stoweidlem20  38713  stoweidlem22  38715  stoweidlem34  38727  stoweidlem44  38737  stoweidlem60  38753  wallispilem3  38760  fourierdlem42  38842  fourierdlem51  38850  fourierdlem54  38853  fourierdlem87  38886  fourierdlem97  38896  ioorrnopnlem  39000  sge0seq  39139  hoicvr  39238  ccatpfx  40073  pfxccat3  40090  upgrewlkle2  40806  wlksoneq1eq2  40870  usgr2trlncl  40964  crctcsh1wlkn0lem5  41015  1wlkiswwlks1  41062  wspthsnwspthsnon  41120  lppthon  41316  upgriseupth  41373  4cyclusnfrgr  41460  av-numclwwlk5  41540  lincresunit3lem3  42055  lindssnlvec  42067
  Copyright terms: Public domain W3C validator