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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl2l  1010  simpr2l  1016  simp12l  1070  simp22l  1076  simp32l  1082  funprg  5440  fsnunf  5870  f1oiso2  6011  omeulem2  6762  uniinqs  6920  unxpdomlem3  7251  gruina  8626  addid2  9181  dmdcan  9656  xaddass  10760  xaddass2  10761  xlt2add  10771  xmulasslem3  10797  xadddi2  10808  xadddi2r  10809  expaddzlem  11350  expaddz  11351  expmulz  11353  expdiv  11357  modexp  11441  ccatopth2  11704  o1add  12334  o1mul  12335  o1sub  12336  prmexpb  13044  pcpremul  13144  pcdiv  13153  pcqmul  13154  pcqdiv  13158  4sqlem12  13251  f1ocpbllem  13676  ercpbl  13701  erlecpbl  13702  latjlej12  14423  latmlem12  14439  latj4  14457  latj4rot  14458  mndodcong  15107  cmn4  15358  ablsub4  15364  abladdsub4  15365  lsm4  15402  abvdom  15853  abvres  15854  abvtrivd  15855  lspsnvs  16113  lspsneu  16122  lspfixed  16127  lspexch  16128  lsmcv  16140  lspsolvlem  16141  coe1sclmulfv  16602  cnprest  17275  hausnei2  17339  isreg2  17363  cmpcld  17387  llyrest  17469  nllyrest  17470  elptr  17526  basqtop  17664  hausflimlem  17932  tmdgsum  18046  utop2nei  18201  trcfilu  18245  ssbl  18345  prdsxmslem2  18449  tgqioo  18702  metnrm  18763  bndth  18854  cph2ass  19046  lmmbr2  19083  iscau3  19102  bcthlem5  19150  ovolunlem2  19261  dvres2  19666  dvfsumlem2  19778  plyadd  20003  plymul  20004  coeeu  20011  coemullem  20035  aalioulem4  20119  mulcxp  20443  cxplea  20454  cxple2  20455  cxplt2  20456  cxpcn3lem  20498  angcan  20511  ang180lem5  20522  divsqrsumlem  20685  logexprlim  20876  dchrvmasumlema  21061  dchrisum0lema  21075  logdivsum  21094  log2sumbnd  21105  abvcxp  21176  padicabv  21191  1pthon  21439  gxmodid  21715  chscllem4  22990  measxun2  24358  measun  24359  mbfmco2  24409  probun  24456  dedekind  24966  ntrivcvgmul  25009  nofulllem5  25384  brbtwn2  25558  axcontlem4  25620  axcontlem8  25624  cgrcomim  25637  cgrcoml  25644  cgrcomr  25645  cgrdegen  25652  btwnintr  25667  btwnexch3  25668  btwnouttr2  25670  btwnouttr  25672  btwnexch  25673  btwndiff  25675  lineid  25731  idinside  25732  btwnconn1lem7  25741  btwnconn1lem8  25742  btwnconn1lem9  25743  btwnconn1lem12  25746  btwnconn1lem14  25748  btwnconn3  25751  midofsegid  25752  segcon2  25753  brsegle2  25757  btwnoutside  25773  outsideoftr  25777  outsideofeu  25779  linethru  25801  cnres2  26163  heibor  26221  mzpsubst  26496  pellexlem5  26587  pellex  26589  pell14qrexpclnn0  26620  pellfundex  26640  qirropth  26662  monotuz  26695  expmordi  26701  congtr  26721  congmul  26723  congsub  26726  mzpcong  26728  fzmaxdif  26737  jm2.15nn0  26765  symgsssg  27077  symgfisg  27078  idomsubgmo  27183  lsmsat  29123  lkrlsp  29217  lkrlsp2  29218  lkrlsp3  29219  latm4  29348  omlspjN  29376  hlatj4  29488  4noncolr3  29567  4noncolr2  29568  4noncolr1  29569  athgt  29570  3dimlem3a  29574  3dimlem4a  29577  3dimlem4  29578  3dimlem4OLDN  29579  3dim3  29583  1cvratex  29587  hlatexch4  29595  3atlem4  29600  atcvrlln2  29633  atcvrlln  29634  lplnnlelln  29657  lvoli2  29695  lvolnlelln  29698  lvolnlelpln  29699  4atlem11b  29722  4atlem12b  29725  2lplnja  29733  2lplnj  29734  dalemyeo  29746  dath2  29851  lncvrat  29896  cdlemblem  29907  cdlemb  29908  elpaddri  29916  padd4N  29954  llnmod2i2  29977  llnexchb2  29983  dalawlem1  29985  dalawlem2  29986  pclfinN  30014  osumcllem6N  30075  pexmidlem3N  30086  lhp2lt  30115  lhp2at0  30146  lhp2atnle  30147  lhp2atne  30148  lhp2at0nle  30149  lhp2at0ne  30150  lhpelim  30151  lhpmod2i2  30152  lhpmod6i1  30153  lhple  30156  lhpat  30157  lhpat3  30160  ltrncoelN  30257  ltrncoat  30258  ltrncnv  30260  trlat  30283  trl0  30284  ltrnnidn  30288  trlnid  30293  cdlemd7  30318  cdleme0b  30326  cdleme0c  30327  cdleme0fN  30332  cdleme02N  30336  cdleme0ex1N  30337  cdleme0ex2N  30338  cdleme7aa  30356  cdleme7c  30359  cdleme7d  30360  cdleme7e  30361  cdleme7ga  30362  cdleme7  30363  cdleme8  30364  cdleme11a  30374  cdleme17c  30402  cdleme22gb  30408  cdlemeda  30412  cdleme20k  30433  cdleme21a  30439  cdleme21d  30444  cdleme22f2  30461  cdleme22g  30462  cdleme23a  30463  cdleme23b  30464  cdleme23c  30465  cdleme24  30466  cdleme28  30487  cdlemefrs32fva1  30515  cdlemefr32sn2aw  30518  cdlemefs32sn1aw  30528  cdleme41sn3a  30547  cdleme32fva  30551  cdleme32fva1  30552  cdleme35a  30562  cdleme35b  30564  cdleme35c  30565  cdleme35f  30568  cdleme39a  30579  cdleme42a  30585  cdleme42c  30586  cdleme42b  30592  cdleme42e  30593  cdleme42f  30594  cdleme42g  30595  cdleme42h  30596  cdleme43bN  30604  cdleme46f2g2  30607  cdleme17d2  30609  cdleme17d4  30611  cdleme48fv  30613  cdleme48fvg  30614  cdleme4gfv  30621  cdlemeg46c  30627  cdlemeg46nlpq  30631  cdlemeg46gfre  30646  cdleme48d  30649  cdlemeg49lebilem  30653  cdleme50trn2  30665  cdleme50ltrn  30671  cdleme  30674  cdlemf1  30675  cdlemf  30677  trlord  30683  ltrniotacnvval  30696  ltrniotavalbN  30698  cdlemg1cex  30702  cdlemg2dN  30704  cdlemg2ce  30706  cdlemg2fvlem  30708  cdlemg2idN  30710  cdlemg2kq  30716  cdlemg2l  30717  cdlemg2m  30718  cdlemg4b2  30724  cdlemg7fvN  30738  cdlemg8a  30741  cdlemg10bALTN  30750  cdlemg11aq  30752  cdlemg12d  30760  cdlemg13a  30765  cdlemg13  30766  cdlemg14f  30767  cdlemg14g  30768  cdlemg17a  30775  cdlemg17b  30776  cdlemg27a  30806  cdlemg31b0N  30808  cdlemg31a  30811  cdlemg31b  30812  cdlemg31c  30813  ltrnco  30833  trlcoabs  30835  trlcoabs2N  30836  trlcocnvat  30838  trlconid  30839  trlcolem  30840  trlcone  30842  cdlemg42  30843  cdlemg43  30844  cdlemg46  30849  cdlemg47  30850  tendoeq1  30878  tendoco2  30882  tendoplco2  30893  tendopltp  30894  cdlemh1  30929  cdlemh2  30930  cdlemi1  30932  cdlemi  30934  cdlemk1  30945  cdlemk2  30946  cdlemk3  30947  cdlemk4  30948  cdlemk8  30952  cdlemk9  30953  cdlemk9bN  30954  cdlemk31  31010  cdlemk32  31011  cdlemk28-3  31022  cdlemk19u  31084  cdlemk56w  31087  tendoex  31089  erngdvlem4  31105  erngdvlem4-rN  31113  dia11N  31163  dib11N  31275  cdlemn6  31317  cdlemn7  31318  cdlemn8  31319  cdlemn9  31320  dihordlem6  31328  dihordlem7  31329  dihord1  31333  dihord2a  31334  dihord2b  31335  dihord2pre  31340  dihord2pre2  31341  dihlsscpre  31349  dihvalcq2  31362  dihopelvalcpre  31363  dihord4  31373  dihord6b  31375  dihmeetlem1N  31405  dihglblem3N  31410  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetcN  31417  dihmeetbclemN  31419  dihmeetlem4preN  31421  dihjatc1  31426  dihjatc2N  31427  dihjatc3  31428  dihmeetlem9N  31430  dihmeetlem13N  31434  dihmeetlem20N  31441  dih1dimatlem0  31443  mapdpglem24  31819  mapdpglem32  31820  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  mapdh9aOLDN  31906  hdmap14lem6  31991
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator