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  4024  tfisi  4651  omeulem1  6582  omeulem2  6583  elfiun  7185  tcrank  7556  isfin2-2  7947  konigthlem  8192  gruen  8436  addid2  8997  mulcan  9407  mulcan2  9408  divass  9444  divdir  9449  div11  9452  divcan5  9464  ltmul1  9608  ltdiv1  9622  ltmuldiv  9628  lediv2  9648  xaddass2  10572  xlt2add  10582  xmulasslem3  10608  xadddi2  10619  expaddz  11148  expmulz  11150  resqrcl  11741  o1add  12089  o1mul  12090  o1sub  12091  dvdsadd2b  12573  dvdsgcd  12724  rpexp12i  12803  pythagtriplem3  12873  pcpremul  12898  pceu  12901  pcqmul  12908  pcqdiv  12912  f1ocpbllem  13428  funcoppc  13751  funcres  13772  catcisolem  13940  1stfcl  13973  2ndfcl  13974  prfcl  13979  evlfcl  13998  curf1cl  14004  curfcl  14008  hofcl  14035  latjlej12  14175  latmlem12  14191  latj4  14209  latj4rot  14210  odcong  14866  cmn4  15110  ablsub4  15116  abladdsub4  15117  lsm4  15154  abvdom  15605  abvres  15606  abvtrivd  15607  lspsolvlem  15897  lbsextlem2  15914  nllyrest  17214  hausflimlem  17676  tsmsxp  17839  xmetlecl  17913  prdsxmetlem  17934  bndth  18458  cph2ass  18650  iscau3  18706  dvres2  19264  coemullem  19633  vieta1  19694  aalioulem4  19717  cxpcn3lem  20089  angcan  20102  dchrvmasumlema  20651  logdivsum  20684  abvcxp  20766  padicabv  20781  gxneg  20935  gxsuc  20941  gxmodid  20948  adjlnop  22668  xreceu  23107  measvunilem  23542  measvunilem0  23543  subdivcomb1  24092  subdivcomb2  24093  ax5seglem3  24561  ax5seglem6  24564  axpasch  24571  axeuclid  24593  axcontlem4  24597  axcontlem8  24601  cgrcomim  24614  cgrcoml  24621  cgrcomr  24622  cgrdegen  24629  segconeu  24636  btwnintr  24644  btwnexch3  24645  btwnouttr2  24647  btwnouttr  24649  btwnexch  24650  trisegint  24653  lineext  24701  linecgr  24706  lineid  24708  idinside  24709  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem7  24718  btwnconn1lem14  24725  btwnconn2  24727  midofsegid  24729  btwnoutside  24750  outsideoftr  24754  lineunray  24772  lineelsb2  24773  uninqs  25050  infxpg  25106  prltub  25271  mulinvsca  25491  truni3  25518  prdnei  25584  supnufb  25641  mulmulvec  25698  distsava  25700  vtarl  25898  cmpmorass  25977  cnres2  26494  heibor  26556  mzpsubst  26837  pellex  26931  pellfundex  26982  pellfund14gap  26983  qirropth  27004  rmxypos  27045  congmul  27065  congsub  27068  mzpcong  27070  coprmdvdsb  27085  jm2.15nn0  27107  jm2.16nn0  27108  rpnnen3lem  27135  symgsssg  27419  symgfisg  27420  psgnunilem4  27431  idomsubgmo  27525  stoweidlem57  27817  bnj1128  29093  lsmcv2  29292  lcvat  29293  lcvexchlem4  29300  lcvexchlem5  29301  lfladd  29329  lflsub  29330  lflmul  29331  lshpkrlem4  29376  latm4  29496  omlmod1i2N  29523  cvlatexch3  29601  cvlsupr7  29611  hlatj4  29636  hlrelat3  29674  cvrval3  29675  atcvrj1  29693  atlelt  29700  2atlt  29701  2atjm  29707  3noncolr2  29711  athgt  29718  3dimlem2  29721  3dimlem4  29726  3dimlem4OLDN  29727  3dim3  29731  1cvratex  29735  ps-1  29739  ps-2  29740  hlatexch3N  29742  llnle  29780  atcvrlln2  29781  atcvrlln  29782  lplni2  29799  lplnle  29802  lplnnle2at  29803  llncvrlpln2  29819  lplnexllnN  29826  2llnmeqat  29833  lvolnle3at  29844  4atlem0ae  29856  lplncvrlvol2  29877  lnjatN  30042  lncvrat  30044  cdlemblem  30055  elpaddri  30064  paddasslem2  30083  paddasslem16  30097  padd4N  30102  hlmod1i  30118  dalawlem2  30134  pclfinN  30162  pexmidlem4N  30235  pl42lem1N  30241  lhp2lt  30263  lhpexle1  30270  lhpexle2lem  30271  lhpj1  30284  lhpmcvr5N  30289  lhp2at0  30294  lhp2atnle  30295  lhp2at0nle  30297  lhple  30304  lhpat  30305  lhpat4N  30306  4atexlempnq  30317  4atexlem7  30337  4atex  30338  ltrn11  30388  ltrnle  30391  ltrnm  30393  ltrnj  30394  ltrncvr  30395  ltrnel  30401  ltrncnvel  30404  ltrncnv  30408  ltrnmw  30413  trlval2  30425  trlcnv  30427  trljat1  30428  trljat2  30429  trlat  30431  trl0  30432  trlnidat  30435  trlnid  30441  cdlemc1  30453  cdlemc2  30454  cdlemc5  30457  cdlemd2  30461  cdlemd7  30466  cdlemd8  30467  cdlemd9  30468  cdleme0e  30479  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme5  30502  cdleme10  30516  cdleme11a  30522  cdleme11c  30523  cdleme11h  30528  cdleme11j  30529  cdleme0nex  30552  cdleme18a  30553  cdleme18b  30554  cdleme22gb  30556  cdleme20zN  30563  cdleme20y  30564  cdleme20c  30573  cdleme20k  30581  cdleme21a  30587  cdleme21b  30588  cdleme21c  30589  cdleme21h  30596  cdleme22b  30603  cdleme22d  30605  cdleme22f  30608  cdleme25a  30615  cdleme25c  30617  cdleme25dN  30618  cdleme26ee  30622  cdleme30a  30640  cdlemefr29bpre0N  30668  cdlemefr29clN  30669  cdlemefr32fvaN  30671  cdlemefr32fva1  30672  cdlemefs29bpre0N  30678  cdlemefs29bpre1N  30679  cdlemefs29cpre1N  30680  cdlemefs29clN  30681  cdleme43fsv1snlem  30682  cdlemefs32fvaN  30684  cdlemefs32fva1  30685  cdlemefs31fv1  30686  cdleme36a  30722  cdleme39a  30727  cdleme42a  30733  cdleme42c  30734  cdleme17d3  30758  cdleme48fv  30761  cdleme48bw  30764  cdleme48b  30765  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfv  30792  cdleme48d  30797  cdleme50trn2a  30812  cdleme50trn2  30813  cdleme50ltrn  30819  cdlemf1  30823  cdlemf  30825  trlord  30831  cdlemg2dN  30852  cdlemg2fvlem  30856  cdlemg2l  30865  cdlemg7fvbwN  30869  cdlemg7aN  30887  cdlemg10bALTN  30898  cdlemg10c  30901  cdlemg17a  30923  cdlemg17dALTN  30926  cdlemg31b0a  30957  cdlemg31a  30959  cdlemg31b  30960  cdlemg34  30974  cdlemg36  30976  ltrnco  30981  trlcoabs2N  30984  trlcolem  30988  cdlemg48  30999  tgrpov  31010  tendoco2  31030  tendoplco2  31041  cdlemh1  31077  cdlemi1  31080  cdlemi2  31081  cdlemj3  31085  tendoid0  31087  cdlemk1  31093  cdlemk2  31094  cdlemk4  31096  cdlemk8  31100  cdlemk9  31101  cdlemk9bN  31102  cdlemk10  31105  cdlemk26b-3  31167  cdlemk26-3  31168  cdlemk28-3  31170  cdlemk37  31176  cdlemk39  31178  cdlemkfid1N  31183  cdlemkid1  31184  cdlemky  31188  cdlemkyu  31189  cdlemk19ylem  31192  cdlemk19xlem  31204  cdlemk11t  31208  cdlemk51  31215  cdlemkyyN  31224  cdleml6  31243  cdleml7  31244  cdleml8  31245  cdleml9  31246  erngdvlem4  31253  erngdvlem4-rN  31261  tendospcanN  31286  dia11N  31311  cdlemm10N  31381  dib11N  31423  dicvaddcl  31453  dicvscacl  31454  cdlemn6  31465  dihvalcq2  31510  dihopelvalcpre  31511  dihord6b  31523  dihord5apre  31525  dihmeetlem1N  31553  dihmeetlem2N  31562  dihglbcpreN  31563  dihjatc1  31574  dihmeetlem20N  31589  dih1dimatlem0  31591  dihatlat  31597  dihglblem6  31603  dochexmidlem4  31726  mapdpglem32  31968  mapdh8ad  32042  mapdh9aOLDN  32054  hdmap11lem2  32108  hdmap14lem6  32139
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