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

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

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 1061 . 2 ((𝜑𝜓𝜒) → 𝜒)
21adantr 481 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simpll3  1100  simprl3  1106  simp1l3  1154  simp2l3  1160  simp3l3  1166  3anandirs  1433  f1prex  6524  fcofo  6528  soisores  6562  weniso  6589  knatar  6592  ofmpteq  6901  smorndom  7450  nnmord  7697  nnmword  7698  difsnen  8027  mapunen  8114  ac6sfi  8189  fipreima  8257  wemaplem2  8437  wemapso2lem  8442  en2eqpr  8815  indcardi  8849  acndom  8859  fodomfi2  8868  infmap2  9025  cflim2  9070  coftr  9080  infpssrlem4  9113  fin23lem11  9124  fincssdom  9130  isf32lem9  9168  fin1a2lem9  9215  gchpwdom  9477  gruima  9609  prpssnq  9797  distrlem4pr  9833  dedekind  10185  addcan  10205  addcan2  10206  divmulass  10693  supmul1  10977  uzsupss  11765  xaddass  12064  xleadd1a  12068  xlesubadd  12078  xmulasslem3  12101  xmulass  12102  xadddilem  12109  xadddi  12110  ixxun  12176  icoshftf1o  12280  snunioc  12285  difelfzle  12436  fzo1fzo0n0  12502  ssfzoulel  12546  modmuladd  12695  modifeq2int  12715  modaddmulmod  12720  modsubdir  12722  ltexp2a  12895  leexp2  12898  ltexp2r  12900  exple1  12903  expnlbnd2  12978  mulsubdivbinom2  13029  hashtpg  13250  ccatass  13354  ccatopth  13452  swrdccatin12lem2a  13466  swrdccat3  13473  cshinj  13538  s2f1o  13642  limsupgre  14193  addcn2  14305  mulcn2  14307  binomrisefac  14754  bpolydif  14767  modmulconst  14994  dvdsmod  15031  sadass  15174  gcdass  15245  rplpwr  15257  rppwr  15258  rpmulgcd2  15351  rpdvds  15355  rpexp  15413  prmdiveq  15472  hashgcdlem  15474  coprimeprodsq  15494  coprimeprodsq2  15495  pythagtriplem3  15504  pcdvdsb  15554  pcgcd1  15562  dvdsprmpweq  15569  pcbc  15585  0ram  15705  ramz2  15709  ramub1lem1  15711  setsstructOLD  15880  mremre  16245  mrieqv2d  16280  lubun  17104  isnsgrp  17269  issubmnd  17299  gsumccat  17359  frmdss2  17381  sgrp2rid2ex  17395  mulgnn0p1  17533  mulgnnsubcl  17534  mulgneg  17541  mulgdirlem  17553  nmzsubg  17616  ghmmulg  17653  pmtrfv  17853  pmtrmvd  17857  pmtrfb  17866  odmodnn0  17940  oddvdsnn0  17944  odnncl  17945  odmod  17946  oddvds  17947  odeq  17950  odmulgid  17952  odmulg  17954  odmulgeq  17955  odbezout  17956  odf1o1  17968  odf1o2  17969  odngen  17973  odcau  18000  pgpssslw  18010  fislw  18021  lsmless1x  18040  lsmless2x  18041  lsmsubm  18049  lsmmod  18069  lsmmod2  18070  efgsfo  18133  cntzcmn  18226  odadd1  18232  odadd2  18233  odadd  18234  lsmcomx  18240  prdscmnd  18245  gsumconst  18315  ring1eq0  18571  cntzsubr  18793  isabvd  18801  rmodislmod  18912  lspss  18965  0lmhm  19021  reslmhm2  19034  pwssplit0  19039  pwssplit1  19040  lbspss  19063  lspfixed  19109  lsmcv  19122  lspsnat  19126  issubassa  19305  aspss  19313  coe1subfv  19617  coe1tm  19624  xrsdsreclblem  19773  obselocv  20053  frlmsplit2  20093  frlmsslss2  20095  frlmup4  20121  lindff1  20140  lsslindf  20150  lsslinds  20151  islindf4  20158  mpt2matmul  20233  mamutpos  20245  submaval  20368  mdetdiag  20386  mdetunilem1  20399  mdetunilem3  20401  mdetunilem9  20407  mdetmul  20410  maducoeval2  20427  madurid  20431  minmar1val  20435  cramer  20478  cpmatel2  20499  m2cpm  20527  decpmatmul  20558  pmatcollpw1lem2  20561  pmatcollpw1  20562  pmatcollpw2lem  20563  pm2mpcl  20583  mply1topmatcl  20591  mp2pm2mplem2  20593  mp2pm2mplem4  20595  pm2mpghmlem2  20598  pm2mpghmlem1  20599  cayhamlem2  20670  neiint  20889  topssnei  20909  cnrest2  21071  cnprest2  21075  cnt0  21131  cnt1  21135  cnhaus  21139  cncmp  21176  fiuncmp  21188  sscmp  21189  hauscmp  21191  cnconn  21206  unconn  21213  comppfsc  21316  kgen2ss  21339  ptpjopn  21396  ptrescn  21423  qtopss  21499  kqfvima  21514  r0cld  21522  cmphaushmeo  21584  fbssint  21623  fbasrn  21669  filuni  21670  ufilmax  21692  fin1aufil  21717  fmf  21730  fmss  21731  rnelfmlem  21737  rnelfm  21738  fmufil  21744  fmco  21746  flimss2  21757  flimss1  21758  flimrest  21768  cnpflf2  21785  cnpflf  21786  flfcnp  21789  lmflf  21790  supnfcls  21805  fclsss1  21807  fclsss2  21808  cnpfcfi  21825  subgntr  21891  opnsubg  21892  cldsubg  21895  ustuqtop1  22026  ucncn  22070  bldisj  22184  blgt0  22185  bl2in  22186  blss2ps  22189  blss2  22190  xbln0  22200  blssps  22210  blss  22211  lpbl  22289  blcld  22291  blcls  22292  stdbdmopn  22304  metcnp2  22328  txmetcnp  22333  blval2  22348  restmetu  22356  nmoix  22514  nmoi2  22515  nmoeq0  22521  nmotri  22524  metdsge  22633  metds0  22634  metdseq0  22638  icoopnst  22719  iccpnfhmeo  22725  xrhmeo  22726  nmhmcn  22901  cphsqrtcl2  22967  cphsqrtcl3  22968  fmcfil  23051  bcthlem5  23106  cmetcusp1  23130  pjth  23191  ovolunnul  23249  volun  23294  voliunlem2  23300  itg2const  23488  iblconst  23565  itgconst  23566  limcvallem  23616  dvcnp2  23664  dvcn  23665  deg1mul3le  23857  deg1tmle  23858  ig1pdvds  23917  coe11  23990  dgrmulc  24008  dvply1  24020  aaliou2  24076  efcvx  24184  tanord  24265  logdivlti  24347  logccv  24390  recxpcl  24402  cxplea  24423  cxple2a  24426  ang180  24525  isosctrlem2  24530  cxp2lim  24684  amgm  24698  muval1  24840  dvdssqf  24845  mumullem2  24887  bcmono  24983  lgsneg  25027  lgsmod  25029  lgsdirprm  25037  lgsdir  25038  lgsdi  25040  brbtwn2  25766  colinearalglem1  25767  colinearalg  25771  axcgrtr  25776  axcontlem2  25826  upgrewlkle2  26483  wlksoneq1eq2  26541  crctcshwlkn0lem5  26687  wspthsnwspthsnon  26792  lppthon  26991  upgriseupth  27047  4cyclusnfrgr  27136  numclwwlk5  27216  nvmul0or  27475  shless  28188  shlej1  28189  pjspansn  28406  kbmul  28784  homco2  28806  kbass2  28946  padct  29471  eliccelico  29513  elicoelioo  29514  iocinioc2  29515  difioo  29518  xrge0npcan  29668  isarchi2  29713  archiabl  29726  mdetlap1  29866  pstmfval  29913  fmcncfil  29951  zrhnm  29987  qqhnm  30008  nexple  30045  volfiniune  30267  omsmeas  30359  eulerpartlemb  30404  probinc  30457  cndprob01  30471  signswmnd  30608  cvmsss2  31230  dvdspw  31611  funsseq  31642  sltres  31789  nolt02olem  31818  nolt02o  31819  nosupbnd1lem1  31828  nosupbnd1lem4  31831  nosupbnd1lem5  31832  nosupbnd1lem6  31833  cgrtriv  32084  5segofs  32088  btwntriv2  32094  btwnxfr  32138  segcon2  32187  brsegle2  32191  seglelin  32198  outsideofeu  32213  lindsenlbs  33375  mblfinlem2  33418  blbnd  33557  rrndstprj2  33601  zerdivemp1x  33717  lsmsat  34114  lsatfixedN  34115  lssat  34122  lkrlsp  34208  lshpkrlem4  34219  cvrcon3b  34383  leat3  34401  atlen0  34416  atnle  34423  atlatmstc  34425  atlatle  34426  cvlcvr1  34445  cvlsupr2  34449  hlsupr2  34492  hlrelat2  34508  cvrexchlem  34524  cvratlem  34526  lnnat  34532  atexchcvrN  34545  1cvratlt  34579  1cvrjat  34580  3atlem3  34590  3atlem7  34594  llni2  34617  atcvrlln2  34624  llnexatN  34626  llncmp  34627  2llnmat  34629  2at0mat0  34630  2atnelpln  34649  llncvrlpln2  34662  2lplnmN  34664  2llnmj  34665  lplncmp  34667  lplnexatN  34668  2llnjaN  34671  lvoli3  34682  islvol2aN  34697  4atlem3a  34702  4atlem4a  34704  4atlem4b  34705  4atlem11  34714  4atlem12  34717  lplncvrlvol2  34720  lvolcmp  34722  2lplnmj  34727  islinei  34845  linepmap  34880  lneq2at  34883  2llnma3r  34893  elpaddn0  34905  elpaddatriN  34908  elpaddat  34909  paddcom  34918  paddss1  34922  paddss2  34923  paddasslem6  34930  paddasslem7  34931  paddasslem10  34934  paddasslem15  34939  pmodlem2  34952  pmodl42N  34956  pmapjoin  34957  atmod1i1m  34963  llnmod1i2  34965  llnexchb2lem  34973  polcon2bN  35025  pclfinclN  35055  poml4N  35058  poml6N  35060  osumcllem11N  35071  osumclN  35072  pmapojoinN  35073  pexmidlem2N  35076  pexmidlem3N  35077  pexmidlem4N  35078  pexmidlem6N  35080  pexmidlem7N  35081  pl42lem2N  35085  pl42lem3N  35086  pl42lem4N  35087  pl42N  35088  lhpexle3lem  35116  lhpmcvr3  35130  lhp2at0nle  35140  lhprelat3N  35145  lauteq  35200  lautco  35202  ltrncoidN  35233  ltrneq2  35253  ltrnnidn  35280  ltrnideq  35281  trlnle  35292  cdlemc  35303  cdlemd4  35307  cdlemd5  35308  cdlemd9  35312  cdlemd  35313  ltrneq3  35314  cdlemefrs29pre00  35502  cdlemefrs29cpre1  35505  cdlemefrs29clN  35506  cdlemefrs32fva  35507  cdlemefr29exN  35509  cdlemefr27cl  35510  cdlemefs27cl  35520  cdlemefs32sn1aw  35521  cdleme32fva  35544  cdleme32d  35551  cdleme32f  35553  cdleme32le  35554  cdleme40n  35575  cdleme41snaw  35583  cdleme17d3  35603  cdleme48fvg  35607  cdlemeg46fvcl  35613  cdlemeg46fgN  35641  cdleme48fgv  35645  ltrniotavalbN  35691  cdlemb3  35713  cdlemg15  35763  cdlemg17dN  35770  trlco  35834  cdlemg44b  35839  ltrncom  35845  trljco  35847  tendococl  35879  tendoplcl  35888  tendoplcom  35889  tendotr  35937  cdlemk36  36020  cdlemk35s-id  36045  cdlemk39s-id  36047  cdlemk19x  36050  cdlemk53b  36063  cdlemk55  36068  cdlemk35u  36071  cdlemk55u  36073  cdlemk39u  36075  cdlemk19u  36077  cdlemk56  36078  tendoex  36082  cdleml5N  36087  dihord2pre  36333  dihord6apre  36364  dihord5b  36367  dihord5apre  36370  dihord  36372  dihmeetlem1N  36398  dihmeetlem2N  36407  dihglbcpreN  36408  dihmeetbN  36411  dihmeetlem4preN  36414  dihmeetlem5  36416  dihmeetlem6  36417  dihmeetlem7N  36418  dihmeetlem10N  36424  dihmeetlem11N  36425  dihmeetlem12N  36426  dihmeetlem13N  36427  dihmeetlem15N  36429  dihmeetlem17N  36431  dihmeetlem18N  36432  dihmeetlem19N  36433  dihmeetALTN  36435  dih1dimatlem0  36436  dihlspsnssN  36440  dvh3dim2  36556  mzpsubst  37130  diophrw  37141  eldioph2lem1  37142  rencldnfi  37204  pellexlem2  37213  pellqrexplicit  37260  infmrgelbi  37261  rmxycomplete  37301  congadd  37352  acongeq  37369  jm2.19  37379  jm2.22  37381  jm2.20nn  37383  jm2.25lem1  37384  jm2.27  37394  jm3.1  37406  lmhmlnmsplit  37476  pwssplit4  37478  hbtlem2  37513  dgraa0p  37538  idomrootle  37592  proot1hash  37597  iocunico  37615  relexpxpmin  37828  brtrclfv2  37838  ntrclsk3  38188  suprnmpt  39171  wessf1ornlem  39187  choicefi  39208  supxrgere  39362  supxrgelem  39366  supxrge  39367  infleinflem2  39400  snunioo1  39541  iccintsng  39552  fmul01  39612  lptre2pt  39672  0ellimcdiv  39681  fnlimfvre  39706  limsupmnfuzlem  39758  limsupgtlem  39803  ibliccsinexp  39929  iblioosinexp  39931  volioc  39951  iblspltprt  39952  stoweidlem20  40000  stoweidlem22  40002  stoweidlem34  40014  stoweidlem44  40024  stoweidlem60  40040  wallispilem3  40047  fourierdlem42  40129  fourierdlem51  40137  fourierdlem54  40140  fourierdlem87  40173  fourierdlem97  40183  ioorrnopnlem  40287  sge0seq  40426  hoicvr  40525  ccatpfx  41174  pfxccat3  41191  lincresunit3lem3  42028  lindssnlvec  42040
  Copyright terms: Public domain W3C validator