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

Theorem simp3l 983
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 443 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl3l  1010  simpr3l  1016  simp13l  1070  simp23l  1076  simp33l  1082  disjss3  4023  tfisi  4648  omeulem1  6576  omeulem2  6577  elfiun  7179  tcrank  7550  isfin2-2  7941  konigthlem  8186  gruen  8430  addid2  8991  mulcan  9401  mulcan2  9402  divass  9438  divdir  9443  div11  9446  divcan5  9458  ltmul1  9602  ltdiv1  9616  ltmuldiv  9622  lediv2  9642  xaddass2  10566  xlt2add  10576  xmulasslem3  10602  xadddi2  10613  expaddz  11142  expmulz  11144  resqrcl  11735  o1add  12083  o1mul  12084  o1sub  12085  dvdsadd2b  12567  dvdsgcd  12718  rpexp12i  12797  pythagtriplem3  12867  pcpremul  12892  pceu  12895  pcqmul  12902  pcqdiv  12906  f1ocpbllem  13422  funcoppc  13745  funcres  13766  catcisolem  13934  1stfcl  13967  2ndfcl  13968  prfcl  13973  evlfcl  13992  curf1cl  13998  curfcl  14002  hofcl  14029  latjlej12  14169  latmlem12  14185  latj4  14203  latj4rot  14204  odcong  14860  cmn4  15104  ablsub4  15110  abladdsub4  15111  lsm4  15148  abvdom  15599  abvres  15600  abvtrivd  15601  lspsolvlem  15891  lbsextlem2  15908  nllyrest  17208  hausflimlem  17670  tsmsxp  17833  xmetlecl  17907  prdsxmetlem  17928  bndth  18452  cph2ass  18644  iscau3  18700  dvres2  19258  coemullem  19627  vieta1  19688  aalioulem4  19711  cxpcn3lem  20083  angcan  20096  dchrvmasumlema  20645  logdivsum  20678  abvcxp  20760  padicabv  20775  gxneg  20927  gxsuc  20933  gxmodid  20940  adjlnop  22662  subdivcomb1  23496  subdivcomb2  23497  axfelem17  23766  ax5seglem3  23969  ax5seglem6  23972  axpasch  23979  axeuclid  24001  axcontlem4  24005  axcontlem8  24009  cgrcomim  24022  cgrcoml  24029  cgrcomr  24030  cgrdegen  24037  segconeu  24044  btwnintr  24052  btwnexch3  24053  btwnouttr2  24055  btwnouttr  24057  btwnexch  24058  trisegint  24061  lineext  24109  linecgr  24114  lineid  24116  idinside  24117  btwnconn1lem3  24122  btwnconn1lem4  24123  btwnconn1lem7  24126  btwnconn1lem14  24133  btwnconn2  24135  midofsegid  24137  btwnoutside  24158  outsideoftr  24162  lineunray  24180  lineelsb2  24181  uninqs  24449  infxpg  24505  prltub  24671  mulinvsca  24891  truni3  24918  prdnei  24984  supnufb  25041  mulmulvec  25098  distsava  25100  vtarl  25298  cmpmorass  25377  cnres2  25894  heibor  25956  mzpsubst  26237  pellex  26331  pellfundex  26382  pellfund14gap  26383  qirropth  26404  rmxypos  26445  congmul  26465  congsub  26468  mzpcong  26470  coprmdvdsb  26485  jm2.15nn0  26507  jm2.16nn0  26508  rpnnen3lem  26535  symgsssg  26819  symgfisg  26820  psgnunilem4  26831  idomsubgmo  26925  stoweidlem57  27217  bnj1128  28299  lsmcv2  28498  lcvat  28499  lcvexchlem4  28506  lcvexchlem5  28507  lfladd  28535  lflsub  28536  lflmul  28537  lshpkrlem4  28582  latm4  28702  omlmod1i2N  28729  cvlatexch3  28807  cvlsupr7  28817  hlatj4  28842  hlrelat3  28880  cvrval3  28881  atcvrj1  28899  atlelt  28906  2atlt  28907  2atjm  28913  3noncolr2  28917  athgt  28924  3dimlem2  28927  3dimlem4  28932  3dimlem4OLDN  28933  3dim3  28937  1cvratex  28941  ps-1  28945  ps-2  28946  hlatexch3N  28948  llnle  28986  atcvrlln2  28987  atcvrlln  28988  lplni2  29005  lplnle  29008  lplnnle2at  29009  llncvrlpln2  29025  lplnexllnN  29032  2llnmeqat  29039  lvolnle3at  29050  4atlem0ae  29062  lplncvrlvol2  29083  lnjatN  29248  lncvrat  29250  cdlemblem  29261  elpaddri  29270  paddasslem2  29289  paddasslem16  29303  padd4N  29308  hlmod1i  29324  dalawlem2  29340  pclfinN  29368  pexmidlem4N  29441  pl42lem1N  29447  lhp2lt  29469  lhpexle1  29476  lhpexle2lem  29477  lhpj1  29490  lhpmcvr5N  29495  lhp2at0  29500  lhp2atnle  29501  lhp2at0nle  29503  lhple  29510  lhpat  29511  lhpat4N  29512  4atexlempnq  29523  4atexlem7  29543  4atex  29544  ltrn11  29594  ltrnle  29597  ltrnm  29599  ltrnj  29600  ltrncvr  29601  ltrnel  29607  ltrncnvel  29610  ltrncnv  29614  ltrnmw  29619  trlval2  29631  trlcnv  29633  trljat1  29634  trljat2  29635  trlat  29637  trl0  29638  trlnidat  29641  trlnid  29647  cdlemc1  29659  cdlemc2  29660  cdlemc5  29663  cdlemd2  29667  cdlemd7  29672  cdlemd8  29673  cdlemd9  29674  cdleme0e  29685  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme5  29708  cdleme10  29722  cdleme11a  29728  cdleme11c  29729  cdleme11h  29734  cdleme11j  29735  cdleme0nex  29758  cdleme18a  29759  cdleme18b  29760  cdleme22gb  29762  cdleme20zN  29769  cdleme20y  29770  cdleme20c  29779  cdleme20k  29787  cdleme21a  29793  cdleme21b  29794  cdleme21c  29795  cdleme21h  29802  cdleme22b  29809  cdleme22d  29811  cdleme22f  29814  cdleme25a  29821  cdleme25c  29823  cdleme25dN  29824  cdleme26ee  29828  cdleme30a  29846  cdlemefr29bpre0N  29874  cdlemefr29clN  29875  cdlemefr32fvaN  29877  cdlemefr32fva1  29878  cdlemefs29bpre0N  29884  cdlemefs29bpre1N  29885  cdlemefs29cpre1N  29886  cdlemefs29clN  29887  cdleme43fsv1snlem  29888  cdlemefs32fvaN  29890  cdlemefs32fva1  29891  cdlemefs31fv1  29892  cdleme36a  29928  cdleme39a  29933  cdleme42a  29939  cdleme42c  29940  cdleme17d3  29964  cdleme48fv  29967  cdleme48bw  29970  cdleme48b  29971  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemeg46gfv  29998  cdleme48d  30003  cdleme50trn2a  30018  cdleme50trn2  30019  cdleme50ltrn  30025  cdlemf1  30029  cdlemf  30031  trlord  30037  cdlemg2dN  30058  cdlemg2fvlem  30062  cdlemg2l  30071  cdlemg7fvbwN  30075  cdlemg7aN  30093  cdlemg10bALTN  30104  cdlemg10c  30107  cdlemg17a  30129  cdlemg17dALTN  30132  cdlemg31b0a  30163  cdlemg31a  30165  cdlemg31b  30166  cdlemg34  30180  cdlemg36  30182  ltrnco  30187  trlcoabs2N  30190  trlcolem  30194  cdlemg48  30205  tgrpov  30216  tendoco2  30236  tendoplco2  30247  cdlemh1  30283  cdlemi1  30286  cdlemi2  30287  cdlemj3  30291  tendoid0  30293  cdlemk1  30299  cdlemk2  30300  cdlemk4  30302  cdlemk8  30306  cdlemk9  30307  cdlemk9bN  30308  cdlemk10  30311  cdlemk26b-3  30373  cdlemk26-3  30374  cdlemk28-3  30376  cdlemk37  30382  cdlemk39  30384  cdlemkfid1N  30389  cdlemkid1  30390  cdlemky  30394  cdlemkyu  30395  cdlemk19ylem  30398  cdlemk19xlem  30410  cdlemk11t  30414  cdlemk51  30421  cdlemkyyN  30430  cdleml6  30449  cdleml7  30450  cdleml8  30451  cdleml9  30452  erngdvlem4  30459  erngdvlem4-rN  30467  tendospcanN  30492  dia11N  30517  cdlemm10N  30587  dib11N  30629  dicvaddcl  30659  dicvscacl  30660  cdlemn6  30671  dihvalcq2  30716  dihopelvalcpre  30717  dihord6b  30729  dihord5apre  30731  dihmeetlem1N  30759  dihmeetlem2N  30768  dihglbcpreN  30769  dihjatc1  30780  dihmeetlem20N  30795  dih1dimatlem0  30797  dihatlat  30803  dihglblem6  30809  dochexmidlem4  30932  mapdpglem32  31174  mapdh8ad  31248  mapdh9aOLDN  31260  hdmap11lem2  31314  hdmap14lem6  31345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator