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

Theorem simp3l 1025
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 455 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1020 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  disjss3  4393  tfisi  6675  tfrlem5  7082  omeulem1  7267  omeulem2  7268  uniinqs  7427  elfiun  7923  tcrank  8333  isfin2-2  8730  konigthlem  8974  gruen  9219  addid2  9796  mulcan  10226  mulcan2  10227  divass  10265  divdir  10270  div11  10273  divcan5  10286  ltmul1  10432  ltdiv1  10446  ltmuldiv  10455  lediv2  10474  xaddass2  11494  xlt2add  11504  xmulasslem3  11530  xadddi2  11541  expaddz  12252  expmulz  12254  resqrtcl  13234  o1add  13583  o1mul  13584  o1sub  13585  dvdsadd2b  14235  dvdsgcd  14388  rpexp12i  14470  pythagtriplem3  14549  pcpremul  14574  pceu  14577  pcqmul  14584  pcqdiv  14588  f1ocpbllem  15136  funcoppc  15486  funcres  15507  catcisolem  15707  1stfcl  15788  2ndfcl  15789  prfcl  15794  evlfcl  15813  curf1cl  15819  curfcl  15823  hofcl  15850  latjlej12  16019  latmlem12  16035  latj4  16053  latj4rot  16054  symgsssg  16814  symgfisg  16815  psgnunilem4  16844  odcong  16895  cmn4  17139  ablsub4  17145  abladdsub4  17146  lsm4  17188  abvdom  17805  abvres  17806  abvtrivd  17807  lspsolvlem  18106  lbsextlem2  18123  lidlsubcl  18181  frlmbas3  19101  matmulcell  19237  marrepeval  19355  ma1repveval  19363  submaeval  19374  mdetunilem3  19406  mdetuni0  19413  mdetmul  19415  minmar1eval  19441  nllyrest  20277  hausflimlem  20770  tsmsxp  20947  psmetlecl  21109  xmetlecl  21139  prdsxmetlem  21161  bndth  21748  cph2ass  21949  iscau3  22007  dvres2  22606  coemullem  22937  vieta1  22998  aalioulem4  23021  cxpcn3lem  23415  angcan  23459  dchrvmasumlema  24064  logdivsum  24097  abvcxp  24179  padicabv  24194  ax5seglem3  24638  ax5seglem6  24641  axpasch  24648  axeuclid  24670  axcontlem4  24674  axcontlem8  24678  clwwlknimp  25180  gxneg  25668  gxsuc  25674  gxmodid  25681  adjlnop  27404  xreceu  28056  orngmul  28232  rhmdvd  28250  measvunilem  28646  measvunilem0  28647  measres  28656  bnj1128  29360  subdivcomb1  29920  subdivcomb2  29921  cgrcomim  30314  cgrcoml  30321  cgrcomr  30322  cgrdegen  30329  segconeu  30336  btwnintr  30344  btwnexch3  30345  btwnouttr2  30347  btwnouttr  30349  btwnexch  30350  trisegint  30353  lineext  30401  linecgr  30406  lineid  30408  idinside  30409  btwnconn1lem3  30414  btwnconn1lem4  30415  btwnconn1lem7  30418  btwnconn1lem14  30425  btwnconn2  30427  midofsegid  30429  btwnoutside  30450  outsideoftr  30454  lineunray  30472  lineelsb2  30473  cnres2  31521  heibor  31579  lsmcv2  32027  lcvat  32028  lcvexchlem4  32035  lcvexchlem5  32036  lfladd  32064  lflsub  32065  lflmul  32066  lshpkrlem4  32111  latm4  32231  omlmod1i2N  32258  cvlatexch3  32336  cvlsupr7  32346  hlatj4  32371  hlrelat3  32409  cvrval3  32410  atcvrj1  32428  atlelt  32435  2atlt  32436  2atjm  32442  3noncolr2  32446  athgt  32453  3dimlem2  32456  3dimlem4  32461  3dimlem4OLDN  32462  3dim3  32466  1cvratex  32470  ps-1  32474  ps-2  32475  hlatexch3N  32477  llnle  32515  atcvrlln2  32516  atcvrlln  32517  lplni2  32534  lplnle  32537  lplnnle2at  32538  llncvrlpln2  32554  lplnexllnN  32561  2llnmeqat  32568  lvolnle3at  32579  4atlem0ae  32591  lplncvrlvol2  32612  lnjatN  32777  lncvrat  32779  cdlemblem  32790  elpaddri  32799  paddasslem2  32818  paddasslem16  32832  padd4N  32837  hlmod1i  32853  dalawlem2  32869  pclfinN  32897  pexmidlem4N  32970  pl42lem1N  32976  lhp2lt  32998  lhpexle1  33005  lhpexle2lem  33006  lhpj1  33019  lhpmcvr5N  33024  lhp2at0  33029  lhp2atnle  33030  lhp2at0nle  33032  lhple  33039  lhpat  33040  lhpat4N  33041  4atexlempnq  33052  4atexlem7  33072  4atex  33073  ltrn11  33123  ltrnle  33126  ltrnm  33128  ltrnj  33129  ltrncvr  33130  ltrnel  33136  ltrncnvel  33139  ltrncnv  33143  ltrnmwOLD  33149  trlval2  33161  trlcnv  33163  trljat1  33164  trljat2  33165  trlat  33167  trl0  33168  trlnidat  33171  trlnid  33177  cdlemc1  33189  cdlemc2  33190  cdlemc5  33193  cdlemd2  33197  cdlemd7  33202  cdlemd8  33203  cdlemd9  33204  cdleme0e  33215  cdleme3g  33232  cdleme3h  33233  cdleme3  33235  cdleme5  33238  cdleme10  33252  cdleme11a  33258  cdleme11c  33259  cdleme11h  33264  cdleme11j  33265  cdleme0nex  33288  cdleme18a  33289  cdleme18b  33290  cdleme22gb  33292  cdleme20zN  33299  cdleme20yOLD  33301  cdleme20c  33310  cdleme20k  33318  cdleme21a  33324  cdleme21b  33325  cdleme21c  33326  cdleme21h  33333  cdleme22b  33340  cdleme22d  33342  cdleme22f  33345  cdleme25a  33352  cdleme25c  33354  cdleme25dN  33355  cdleme26ee  33359  cdleme30a  33377  cdlemefr29bpre0N  33405  cdlemefr29clN  33406  cdlemefr32fvaN  33408  cdlemefr32fva1  33409  cdlemefs29bpre0N  33415  cdlemefs29bpre1N  33416  cdlemefs29cpre1N  33417  cdlemefs29clN  33418  cdleme43fsv1snlem  33419  cdlemefs32fvaN  33421  cdlemefs32fva1  33422  cdlemefs31fv1  33423  cdleme36a  33459  cdleme39a  33464  cdleme42a  33470  cdleme42c  33471  cdleme17d3  33495  cdleme48fv  33498  cdleme48bw  33501  cdleme48b  33502  cdlemeg46rgv  33527  cdlemeg46req  33528  cdlemeg46gfv  33529  cdleme48d  33534  cdleme50trn2a  33549  cdleme50trn2  33550  cdleme50ltrn  33556  cdlemf1  33560  cdlemf  33562  trlord  33568  cdlemg2dN  33589  cdlemg2fvlem  33593  cdlemg2l  33602  cdlemg7fvbwN  33606  cdlemg7aN  33624  cdlemg10bALTN  33635  cdlemg10c  33638  cdlemg17a  33660  cdlemg17dALTN  33663  cdlemg31b0a  33694  cdlemg31a  33696  cdlemg31b  33697  cdlemg34  33711  cdlemg36  33713  ltrnco  33718  trlcoabs2N  33721  trlcolem  33725  cdlemg48  33736  tgrpov  33747  tendoco2  33767  tendoplco2  33778  cdlemh1  33814  cdlemi1  33817  cdlemi2  33818  cdlemj3  33822  tendoid0  33824  cdlemk1  33830  cdlemk2  33831  cdlemk4  33833  cdlemk8  33837  cdlemk9  33838  cdlemk9bN  33839  cdlemk10  33842  cdlemk26b-3  33904  cdlemk26-3  33905  cdlemk28-3  33907  cdlemk37  33913  cdlemk39  33915  cdlemkfid1N  33920  cdlemkid1  33921  cdlemky  33925  cdlemkyu  33926  cdlemk19ylem  33929  cdlemk19xlem  33941  cdlemk11t  33945  cdlemk51  33952  cdlemkyyN  33961  cdleml6  33980  cdleml7  33981  cdleml8  33982  cdleml9  33983  erngdvlem4  33990  erngdvlem4-rN  33998  tendospcanN  34023  dia11N  34048  cdlemm10N  34118  dib11N  34160  dicvaddcl  34190  dicvscacl  34191  cdlemn6  34202  dihvalcq2  34247  dihopelvalcpre  34248  dihord6b  34260  dihord5apre  34262  dihmeetlem1N  34290  dihmeetlem2N  34299  dihglbcpreN  34300  dihjatc1  34311  dihmeetlem20N  34326  dih1dimatlem0  34328  dihatlat  34334  dihglblem6  34340  dochexmidlem4  34463  mapdpglem32  34705  mapdh8ad  34779  mapdh9aOLDN  34791  hdmap11lem2  34845  hdmap14lem6  34876  mzpsubst  35022  pellex  35112  pellfundex  35163  pellfund14gap  35164  qirropth  35185  rmxypos  35226  congmul  35246  congsub  35249  mzpcong  35251  coprmdvdsb  35266  jm2.15nn0  35287  jm2.16nn0  35288  rpnnen3lem  35315  idomsubgmo  35499  relexp01min  35672  mullimc  36971  islptre  36974  limccog  36975  mullimcf  36978  addlimc  37003  0ellimcdiv  37004  stoweidlem57  37188  fourierdlem48  37286  fourierdlem80  37318  fourierdlem113  37351
  Copyright terms: Public domain W3C validator