MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3l Structured version   Unicode version

Theorem simp3l 1024
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 457 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1019 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  simpl3l  1051  simpr3l  1057  simp13l  1111  simp23l  1117  simp33l  1123  disjss3  4455  tfisi  6692  tfrlem5  7067  omeulem1  7249  omeulem2  7250  uniinqs  7409  elfiun  7908  tcrank  8319  isfin2-2  8716  konigthlem  8960  gruen  9207  addid2  9780  mulcan  10207  mulcan2  10208  divass  10246  divdir  10251  div11  10254  divcan5  10267  ltmul1  10413  ltdiv1  10427  ltmuldiv  10436  lediv2  10455  xaddass2  11467  xlt2add  11477  xmulasslem3  11503  xadddi2  11514  expaddz  12213  expmulz  12215  resqrtcl  13099  o1add  13448  o1mul  13449  o1sub  13450  dvdsadd2b  14040  dvdsgcd  14193  rpexp12i  14275  pythagtriplem3  14354  pcpremul  14379  pceu  14382  pcqmul  14389  pcqdiv  14393  f1ocpbllem  14941  funcoppc  15291  funcres  15312  catcisolem  15512  1stfcl  15593  2ndfcl  15594  prfcl  15599  evlfcl  15618  curf1cl  15624  curfcl  15628  hofcl  15655  latjlej12  15824  latmlem12  15840  latj4  15858  latj4rot  15859  symgsssg  16619  symgfisg  16620  psgnunilem4  16649  odcong  16700  cmn4  16944  ablsub4  16950  abladdsub4  16951  lsm4  16993  abvdom  17614  abvres  17615  abvtrivd  17616  lspsolvlem  17915  lbsextlem2  17932  lidlsubcl  17990  frlmbas3  18934  matmulcell  19074  marrepeval  19192  ma1repveval  19200  submaeval  19211  mdetunilem3  19243  mdetuni0  19250  mdetmul  19252  minmar1eval  19278  nllyrest  20113  hausflimlem  20606  tsmsxp  20783  psmetlecl  20945  xmetlecl  20975  prdsxmetlem  20997  bndth  21584  cph2ass  21785  iscau3  21843  dvres2  22442  coemullem  22773  vieta1  22834  aalioulem4  22857  cxpcn3lem  23247  angcan  23260  dchrvmasumlema  23811  logdivsum  23844  abvcxp  23926  padicabv  23941  ax5seglem3  24361  ax5seglem6  24364  axpasch  24371  axeuclid  24393  axcontlem4  24397  axcontlem8  24401  clwwlknimp  24903  gxneg  25395  gxsuc  25401  gxmodid  25408  adjlnop  27132  xreceu  27778  orngmul  27954  rhmdvd  27972  measvunilem  28356  measvunilem0  28357  measres  28366  subdivcomb1  29323  subdivcomb2  29324  cgrcomim  29844  cgrcoml  29851  cgrcomr  29852  cgrdegen  29859  segconeu  29866  btwnintr  29874  btwnexch3  29875  btwnouttr2  29877  btwnouttr  29879  btwnexch  29880  trisegint  29883  lineext  29931  linecgr  29936  lineid  29938  idinside  29939  btwnconn1lem3  29944  btwnconn1lem4  29945  btwnconn1lem7  29948  btwnconn1lem14  29955  btwnconn2  29957  midofsegid  29959  btwnoutside  29980  outsideoftr  29984  lineunray  30002  lineelsb2  30003  cnres2  30464  heibor  30522  mzpsubst  30886  pellex  30975  pellfundex  31026  pellfund14gap  31027  qirropth  31048  rmxypos  31089  congmul  31109  congsub  31112  mzpcong  31114  coprmdvdsb  31129  jm2.15nn0  31149  jm2.16nn0  31150  rpnnen3lem  31177  idomsubgmo  31359  mullimc  31825  islptre  31828  limccog  31829  mullimcf  31832  addlimc  31857  0ellimcdiv  31858  stoweidlem57  32042  fourierdlem48  32140  fourierdlem80  32172  fourierdlem113  32205  bnj1128  34189  lsmcv2  34897  lcvat  34898  lcvexchlem4  34905  lcvexchlem5  34906  lfladd  34934  lflsub  34935  lflmul  34936  lshpkrlem4  34981  latm4  35101  omlmod1i2N  35128  cvlatexch3  35206  cvlsupr7  35216  hlatj4  35241  hlrelat3  35279  cvrval3  35280  atcvrj1  35298  atlelt  35305  2atlt  35306  2atjm  35312  3noncolr2  35316  athgt  35323  3dimlem2  35326  3dimlem4  35331  3dimlem4OLDN  35332  3dim3  35336  1cvratex  35340  ps-1  35344  ps-2  35345  hlatexch3N  35347  llnle  35385  atcvrlln2  35386  atcvrlln  35387  lplni2  35404  lplnle  35407  lplnnle2at  35408  llncvrlpln2  35424  lplnexllnN  35431  2llnmeqat  35438  lvolnle3at  35449  4atlem0ae  35461  lplncvrlvol2  35482  lnjatN  35647  lncvrat  35649  cdlemblem  35660  elpaddri  35669  paddasslem2  35688  paddasslem16  35702  padd4N  35707  hlmod1i  35723  dalawlem2  35739  pclfinN  35767  pexmidlem4N  35840  pl42lem1N  35846  lhp2lt  35868  lhpexle1  35875  lhpexle2lem  35876  lhpj1  35889  lhpmcvr5N  35894  lhp2at0  35899  lhp2atnle  35900  lhp2at0nle  35902  lhple  35909  lhpat  35910  lhpat4N  35911  4atexlempnq  35922  4atexlem7  35942  4atex  35943  ltrn11  35993  ltrnle  35996  ltrnm  35998  ltrnj  35999  ltrncvr  36000  ltrnel  36006  ltrncnvel  36009  ltrncnv  36013  ltrnmwOLD  36019  trlval2  36031  trlcnv  36033  trljat1  36034  trljat2  36035  trlat  36037  trl0  36038  trlnidat  36041  trlnid  36047  cdlemc1  36059  cdlemc2  36060  cdlemc5  36063  cdlemd2  36067  cdlemd7  36072  cdlemd8  36073  cdlemd9  36074  cdleme0e  36085  cdleme3g  36102  cdleme3h  36103  cdleme3  36105  cdleme5  36108  cdleme10  36122  cdleme11a  36128  cdleme11c  36129  cdleme11h  36134  cdleme11j  36135  cdleme0nex  36158  cdleme18a  36159  cdleme18b  36160  cdleme22gb  36162  cdleme20zN  36169  cdleme20yOLD  36171  cdleme20c  36180  cdleme20k  36188  cdleme21a  36194  cdleme21b  36195  cdleme21c  36196  cdleme21h  36203  cdleme22b  36210  cdleme22d  36212  cdleme22f  36215  cdleme25a  36222  cdleme25c  36224  cdleme25dN  36225  cdleme26ee  36229  cdleme30a  36247  cdlemefr29bpre0N  36275  cdlemefr29clN  36276  cdlemefr32fvaN  36278  cdlemefr32fva1  36279  cdlemefs29bpre0N  36285  cdlemefs29bpre1N  36286  cdlemefs29cpre1N  36287  cdlemefs29clN  36288  cdleme43fsv1snlem  36289  cdlemefs32fvaN  36291  cdlemefs32fva1  36292  cdlemefs31fv1  36293  cdleme36a  36329  cdleme39a  36334  cdleme42a  36340  cdleme42c  36341  cdleme17d3  36365  cdleme48fv  36368  cdleme48bw  36371  cdleme48b  36372  cdlemeg46rgv  36397  cdlemeg46req  36398  cdlemeg46gfv  36399  cdleme48d  36404  cdleme50trn2a  36419  cdleme50trn2  36420  cdleme50ltrn  36426  cdlemf1  36430  cdlemf  36432  trlord  36438  cdlemg2dN  36459  cdlemg2fvlem  36463  cdlemg2l  36472  cdlemg7fvbwN  36476  cdlemg7aN  36494  cdlemg10bALTN  36505  cdlemg10c  36508  cdlemg17a  36530  cdlemg17dALTN  36533  cdlemg31b0a  36564  cdlemg31a  36566  cdlemg31b  36567  cdlemg34  36581  cdlemg36  36583  ltrnco  36588  trlcoabs2N  36591  trlcolem  36595  cdlemg48  36606  tgrpov  36617  tendoco2  36637  tendoplco2  36648  cdlemh1  36684  cdlemi1  36687  cdlemi2  36688  cdlemj3  36692  tendoid0  36694  cdlemk1  36700  cdlemk2  36701  cdlemk4  36703  cdlemk8  36707  cdlemk9  36708  cdlemk9bN  36709  cdlemk10  36712  cdlemk26b-3  36774  cdlemk26-3  36775  cdlemk28-3  36777  cdlemk37  36783  cdlemk39  36785  cdlemkfid1N  36790  cdlemkid1  36791  cdlemky  36795  cdlemkyu  36796  cdlemk19ylem  36799  cdlemk19xlem  36811  cdlemk11t  36815  cdlemk51  36822  cdlemkyyN  36831  cdleml6  36850  cdleml7  36851  cdleml8  36852  cdleml9  36853  erngdvlem4  36860  erngdvlem4-rN  36868  tendospcanN  36893  dia11N  36918  cdlemm10N  36988  dib11N  37030  dicvaddcl  37060  dicvscacl  37061  cdlemn6  37072  dihvalcq2  37117  dihopelvalcpre  37118  dihord6b  37130  dihord5apre  37132  dihmeetlem1N  37160  dihmeetlem2N  37169  dihglbcpreN  37170  dihjatc1  37181  dihmeetlem20N  37196  dih1dimatlem0  37198  dihatlat  37204  dihglblem6  37210  dochexmidlem4  37333  mapdpglem32  37575  mapdh8ad  37649  mapdh9aOLDN  37661  hdmap11lem2  37715  hdmap14lem6  37746
  Copyright terms: Public domain W3C validator