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

Theorem simp3l 1009
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 454 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1004 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  simpl3l  1036  simpr3l  1042  simp13l  1096  simp23l  1102  simp33l  1108  disjss3  4279  tfisi  6458  tfrlem5  6825  omeulem1  7009  omeulem2  7010  uniinqs  7168  elfiun  7668  tcrank  8079  isfin2-2  8476  konigthlem  8720  gruen  8966  addid2  9539  mulcan  9960  mulcan2  9961  divass  9999  divdir  10004  div11  10007  divcan5  10020  ltmul1  10166  ltdiv1  10180  ltmuldiv  10189  lediv2  10209  xaddass2  11200  xlt2add  11210  xmulasslem3  11236  xadddi2  11247  expaddz  11891  expmulz  11893  resqrcl  12726  o1add  13074  o1mul  13075  o1sub  13076  dvdsadd2b  13557  dvdsgcd  13709  rpexp12i  13790  pythagtriplem3  13867  pcpremul  13892  pceu  13895  pcqmul  13902  pcqdiv  13906  f1ocpbllem  14444  funcoppc  14767  funcres  14788  catcisolem  14956  1stfcl  14989  2ndfcl  14990  prfcl  14995  evlfcl  15014  curf1cl  15020  curfcl  15024  hofcl  15051  latjlej12  15219  latmlem12  15235  latj4  15253  latj4rot  15254  symgsssg  15952  symgfisg  15953  psgnunilem4  15982  odcong  16031  cmn4  16275  ablsub4  16281  abladdsub4  16282  lsm4  16321  abvdom  16846  abvres  16847  abvtrivd  16848  lspsolvlem  17144  lbsextlem2  17161  frlmbas3  18042  marrepeval  18215  ma1repveval  18223  submaeval  18234  mdetunilem3  18261  mdetuni0  18268  mdetmul  18270  minmar1eval  18296  nllyrest  18931  hausflimlem  19393  tsmsxp  19570  psmetlecl  19732  xmetlecl  19762  prdsxmetlem  19784  bndth  20371  cph2ass  20572  iscau3  20630  dvres2  21228  coemullem  21601  vieta1  21662  aalioulem4  21685  cxpcn3lem  22069  angcan  22082  dchrvmasumlema  22633  logdivsum  22666  abvcxp  22748  padicabv  22763  ax5seglem3  22999  ax5seglem6  23002  axpasch  23009  axeuclid  23031  axcontlem4  23035  axcontlem8  23039  gxneg  23575  gxsuc  23581  gxmodid  23588  adjlnop  25312  xreceu  25919  orngmul  26123  rhmdvd  26141  measvunilem  26479  measvunilem0  26480  measres  26489  subdivcomb1  27230  subdivcomb2  27231  cgrcomim  27866  cgrcoml  27873  cgrcomr  27874  cgrdegen  27881  segconeu  27888  btwnintr  27896  btwnexch3  27897  btwnouttr2  27899  btwnouttr  27901  btwnexch  27902  trisegint  27905  lineext  27953  linecgr  27958  lineid  27960  idinside  27961  btwnconn1lem3  27966  btwnconn1lem4  27967  btwnconn1lem7  27970  btwnconn1lem14  27977  btwnconn2  27979  midofsegid  27981  btwnoutside  28002  outsideoftr  28006  lineunray  28024  lineelsb2  28025  cnres2  28503  heibor  28561  mzpsubst  28927  pellex  29018  pellfundex  29069  pellfund14gap  29070  qirropth  29091  rmxypos  29132  congmul  29152  congsub  29155  mzpcong  29157  coprmdvdsb  29172  jm2.15nn0  29194  jm2.16nn0  29195  rpnnen3lem  29222  idomsubgmo  29405  stoweidlem57  29695  clwwlknimp  30282  bnj1128  31680  lsmcv2  32244  lcvat  32245  lcvexchlem4  32252  lcvexchlem5  32253  lfladd  32281  lflsub  32282  lflmul  32283  lshpkrlem4  32328  latm4  32448  omlmod1i2N  32475  cvlatexch3  32553  cvlsupr7  32563  hlatj4  32588  hlrelat3  32626  cvrval3  32627  atcvrj1  32645  atlelt  32652  2atlt  32653  2atjm  32659  3noncolr2  32663  athgt  32670  3dimlem2  32673  3dimlem4  32678  3dimlem4OLDN  32679  3dim3  32683  1cvratex  32687  ps-1  32691  ps-2  32692  hlatexch3N  32694  llnle  32732  atcvrlln2  32733  atcvrlln  32734  lplni2  32751  lplnle  32754  lplnnle2at  32755  llncvrlpln2  32771  lplnexllnN  32778  2llnmeqat  32785  lvolnle3at  32796  4atlem0ae  32808  lplncvrlvol2  32829  lnjatN  32994  lncvrat  32996  cdlemblem  33007  elpaddri  33016  paddasslem2  33035  paddasslem16  33049  padd4N  33054  hlmod1i  33070  dalawlem2  33086  pclfinN  33114  pexmidlem4N  33187  pl42lem1N  33193  lhp2lt  33215  lhpexle1  33222  lhpexle2lem  33223  lhpj1  33236  lhpmcvr5N  33241  lhp2at0  33246  lhp2atnle  33247  lhp2at0nle  33249  lhple  33256  lhpat  33257  lhpat4N  33258  4atexlempnq  33269  4atexlem7  33289  4atex  33290  ltrn11  33340  ltrnle  33343  ltrnm  33345  ltrnj  33346  ltrncvr  33347  ltrnel  33353  ltrncnvel  33356  ltrncnv  33360  ltrnmw  33365  trlval2  33377  trlcnv  33379  trljat1  33380  trljat2  33381  trlat  33383  trl0  33384  trlnidat  33387  trlnid  33393  cdlemc1  33405  cdlemc2  33406  cdlemc5  33409  cdlemd2  33413  cdlemd7  33418  cdlemd8  33419  cdlemd9  33420  cdleme0e  33431  cdleme3g  33448  cdleme3h  33449  cdleme3  33451  cdleme5  33454  cdleme10  33468  cdleme11a  33474  cdleme11c  33475  cdleme11h  33480  cdleme11j  33481  cdleme0nex  33504  cdleme18a  33505  cdleme18b  33506  cdleme22gb  33508  cdleme20zN  33515  cdleme20y  33516  cdleme20c  33525  cdleme20k  33533  cdleme21a  33539  cdleme21b  33540  cdleme21c  33541  cdleme21h  33548  cdleme22b  33555  cdleme22d  33557  cdleme22f  33560  cdleme25a  33567  cdleme25c  33569  cdleme25dN  33570  cdleme26ee  33574  cdleme30a  33592  cdlemefr29bpre0N  33620  cdlemefr29clN  33621  cdlemefr32fvaN  33623  cdlemefr32fva1  33624  cdlemefs29bpre0N  33630  cdlemefs29bpre1N  33631  cdlemefs29cpre1N  33632  cdlemefs29clN  33633  cdleme43fsv1snlem  33634  cdlemefs32fvaN  33636  cdlemefs32fva1  33637  cdlemefs31fv1  33638  cdleme36a  33674  cdleme39a  33679  cdleme42a  33685  cdleme42c  33686  cdleme17d3  33710  cdleme48fv  33713  cdleme48bw  33716  cdleme48b  33717  cdlemeg46rgv  33742  cdlemeg46req  33743  cdlemeg46gfv  33744  cdleme48d  33749  cdleme50trn2a  33764  cdleme50trn2  33765  cdleme50ltrn  33771  cdlemf1  33775  cdlemf  33777  trlord  33783  cdlemg2dN  33804  cdlemg2fvlem  33808  cdlemg2l  33817  cdlemg7fvbwN  33821  cdlemg7aN  33839  cdlemg10bALTN  33850  cdlemg10c  33853  cdlemg17a  33875  cdlemg17dALTN  33878  cdlemg31b0a  33909  cdlemg31a  33911  cdlemg31b  33912  cdlemg34  33926  cdlemg36  33928  ltrnco  33933  trlcoabs2N  33936  trlcolem  33940  cdlemg48  33951  tgrpov  33962  tendoco2  33982  tendoplco2  33993  cdlemh1  34029  cdlemi1  34032  cdlemi2  34033  cdlemj3  34037  tendoid0  34039  cdlemk1  34045  cdlemk2  34046  cdlemk4  34048  cdlemk8  34052  cdlemk9  34053  cdlemk9bN  34054  cdlemk10  34057  cdlemk26b-3  34119  cdlemk26-3  34120  cdlemk28-3  34122  cdlemk37  34128  cdlemk39  34130  cdlemkfid1N  34135  cdlemkid1  34136  cdlemky  34140  cdlemkyu  34141  cdlemk19ylem  34144  cdlemk19xlem  34156  cdlemk11t  34160  cdlemk51  34167  cdlemkyyN  34176  cdleml6  34195  cdleml7  34196  cdleml8  34197  cdleml9  34198  erngdvlem4  34205  erngdvlem4-rN  34213  tendospcanN  34238  dia11N  34263  cdlemm10N  34333  dib11N  34375  dicvaddcl  34405  dicvscacl  34406  cdlemn6  34417  dihvalcq2  34462  dihopelvalcpre  34463  dihord6b  34475  dihord5apre  34477  dihmeetlem1N  34505  dihmeetlem2N  34514  dihglbcpreN  34515  dihjatc1  34526  dihmeetlem20N  34541  dih1dimatlem0  34543  dihatlat  34549  dihglblem6  34555  dochexmidlem4  34678  mapdpglem32  34920  mapdh8ad  34994  mapdh9aOLDN  35006  hdmap11lem2  35060  hdmap14lem6  35091
  Copyright terms: Public domain W3C validator