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

Theorem simp2l 1031
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 458 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1027 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl2l  1058  simpr2l  1064  simp12l  1118  simp22l  1124  simp32l  1130  funprg  5593  fsnunf  6061  f1oiso2  6202  omeulem2  7239  uniinqs  7398  unxpdomlem3  7731  gruina  9194  dedekind  9748  addid2  9767  dmdcan  10268  xaddass  11486  xaddass2  11487  xlt2add  11497  xmulasslem3  11523  xadddi2  11534  xadddi2r  11535  expaddzlem  12265  expaddz  12266  expmulz  12268  expdiv  12273  modexp  12357  ccatopth2  12773  swrdco  12880  o1add  13620  o1mul  13621  o1sub  13622  ntrivcvgmul  13901  prmexpb  14613  pcpremul  14736  pcdiv  14745  pcqmul  14746  pcqdiv  14750  4sqlem12  14843  f1ocpbllem  15373  ercpbl  15398  erlecpbl  15399  latjlej12  16256  latmlem12  16272  latj4  16290  latj4rot  16291  symgsssg  17051  symgfisg  17052  mndodcong  17134  cmn4  17392  ablsub4  17398  abladdsub4  17399  lsm4  17441  abvdom  18009  abvres  18010  abvtrivd  18011  lspsnvs  18280  lspsneu  18289  lspfixed  18294  lspexch  18295  lsmcv  18307  lspsolvlem  18308  coe1sclmulfv  18819  matvscacell  19403  m1detdiag  19564  cramerimplem3  19652  cnprest  20247  hausnei2  20311  isreg2  20335  cmpcld  20359  llyrest  20442  nllyrest  20443  elptr  20530  basqtop  20668  hausflimlem  20936  tmdgsum  21052  utop2nei  21207  trcfilu  21251  ssblps  21379  ssbl  21380  prdsxmslem2  21486  tgqioo  21760  metnrm  21836  bndth  21928  cph2ass  22132  lmmbr2  22171  iscau3  22190  bcthlem5  22238  ovolunlem2  22393  dvres2  22809  dvfsumlem2  22921  plyadd  23113  plymul  23114  coeeu  23121  coemullem  23146  aalioulem4  23233  mulcxp  23572  cxplea  23583  cxple2  23584  cxplt2  23585  cxpcn3lem  23629  angcan  23673  ang180lem5  23684  divsqrtsumlem  23847  logexprlim  24095  dchrvmasumlema  24280  dchrisum0lema  24294  logdivsum  24313  log2sumbnd  24324  abvcxp  24395  padicabv  24410  tghilberti2  24625  brbtwn2  24877  axcontlem4  24939  axcontlem8  24943  1pthon  25263  clwwlkel  25463  gxmodid  25949  chscllem4  27235  orngmul  28518  measxun2  28984  measun  28985  mbfmco2  29039  probun  29204  nofulllem5  30544  cgrcomim  30705  cgrcoml  30712  cgrcomr  30713  cgrdegen  30720  btwnintr  30735  btwnexch3  30736  btwnouttr2  30738  btwnouttr  30740  btwnexch  30741  btwndiff  30743  lineid  30799  idinside  30800  btwnconn1lem7  30809  btwnconn1lem8  30810  btwnconn1lem9  30811  btwnconn1lem12  30814  btwnconn1lem14  30816  btwnconn3  30819  midofsegid  30820  segcon2  30821  brsegle2  30825  btwnoutside  30841  outsideoftr  30845  outsideofeu  30847  linethru  30869  cnres2  32002  heibor  32060  lsmsat  32486  lkrlsp  32580  lkrlsp2  32581  lkrlsp3  32582  latm4  32711  omlspjN  32739  hlatj4  32851  4noncolr3  32930  4noncolr2  32931  4noncolr1  32932  athgt  32933  3dimlem3a  32937  3dimlem4a  32940  3dimlem4  32941  3dimlem4OLDN  32942  3dim3  32946  1cvratex  32950  hlatexch4  32958  3atlem4  32963  atcvrlln2  32996  atcvrlln  32997  lplnnlelln  33020  lvoli2  33058  lvolnlelln  33061  lvolnlelpln  33062  4atlem11b  33085  4atlem12b  33088  2lplnja  33096  2lplnj  33097  dalemyeo  33109  dath2  33214  lncvrat  33259  cdlemblem  33270  cdlemb  33271  elpaddri  33279  padd4N  33317  llnmod2i2  33340  llnexchb2  33346  dalawlem1  33348  dalawlem2  33349  pclfinN  33377  osumcllem6N  33438  pexmidlem3N  33449  lhp2lt  33478  lhp2at0  33509  lhp2atnle  33510  lhp2atne  33511  lhp2at0nle  33512  lhp2at0ne  33513  lhpelim  33514  lhpmod2i2  33515  lhpmod6i1  33516  lhple  33519  lhpat  33520  lhpat3  33523  ltrncoelN  33620  ltrncoat  33621  ltrncnv  33623  trlat  33647  trl0  33648  ltrnnidn  33652  trlnid  33657  cdlemd7  33682  cdleme0b  33690  cdleme0c  33691  cdleme0fN  33696  cdleme02N  33700  cdleme0ex1N  33701  cdleme0ex2N  33702  cdleme7aa  33720  cdleme7c  33723  cdleme7d  33724  cdleme7e  33725  cdleme7ga  33726  cdleme7  33727  cdleme8  33728  cdleme11a  33738  cdleme17c  33766  cdleme22gb  33772  cdlemeda  33776  cdleme20k  33798  cdleme21a  33804  cdleme21d  33809  cdleme22f2  33826  cdleme22g  33827  cdleme23a  33828  cdleme23b  33829  cdleme23c  33830  cdleme24  33831  cdleme28  33852  cdlemefrs32fva1  33880  cdlemefr32sn2aw  33883  cdlemefs32sn1aw  33893  cdleme41sn3a  33912  cdleme32fva  33916  cdleme32fva1  33917  cdleme35a  33927  cdleme35b  33929  cdleme35c  33930  cdleme35f  33933  cdleme39a  33944  cdleme42a  33950  cdleme42c  33951  cdleme42b  33957  cdleme42e  33958  cdleme42f  33959  cdleme42g  33960  cdleme42h  33961  cdleme43bN  33969  cdleme46f2g2  33972  cdleme17d2  33974  cdleme17d4  33976  cdleme48fv  33978  cdleme48fvg  33979  cdleme4gfv  33986  cdlemeg46c  33992  cdlemeg46nlpq  33996  cdlemeg46gfre  34011  cdleme48d  34014  cdlemeg49lebilem  34018  cdleme50trn2  34030  cdleme50ltrn  34036  cdleme  34039  cdlemf1  34040  cdlemf  34042  trlord  34048  ltrniotacnvval  34061  ltrniotavalbN  34063  cdlemg1cex  34067  cdlemg2dN  34069  cdlemg2ce  34071  cdlemg2fvlem  34073  cdlemg2idN  34075  cdlemg2kq  34081  cdlemg2l  34082  cdlemg2m  34083  cdlemg4b2  34089  cdlemg7fvN  34103  cdlemg8a  34106  cdlemg10bALTN  34115  cdlemg11aq  34117  cdlemg12d  34125  cdlemg13a  34130  cdlemg13  34131  cdlemg14f  34132  cdlemg14g  34133  cdlemg17a  34140  cdlemg17b  34141  cdlemg27a  34171  cdlemg31b0N  34173  cdlemg31a  34176  cdlemg31b  34177  cdlemg31c  34178  ltrnco  34198  trlcoabs  34200  trlcoabs2N  34201  trlcocnvat  34203  trlconid  34204  trlcolem  34205  trlcone  34207  cdlemg42  34208  cdlemg43  34209  cdlemg46  34214  cdlemg47  34215  tendoeq1  34243  tendoco2  34247  tendoplco2  34258  tendopltp  34259  cdlemh1  34294  cdlemh2  34295  cdlemi1  34297  cdlemi  34299  cdlemk1  34310  cdlemk2  34311  cdlemk3  34312  cdlemk4  34313  cdlemk8  34317  cdlemk9  34318  cdlemk9bN  34319  cdlemk31  34375  cdlemk32  34376  cdlemk28-3  34387  cdlemk19u  34449  cdlemk56w  34452  tendoex  34454  erngdvlem4  34470  erngdvlem4-rN  34478  dia11N  34528  dib11N  34640  cdlemn6  34682  cdlemn7  34683  cdlemn8  34684  cdlemn9  34685  dihordlem6  34693  dihordlem7  34694  dihord1  34698  dihord2a  34699  dihord2b  34700  dihord2pre  34705  dihord2pre2  34706  dihlsscpre  34714  dihvalcq2  34727  dihopelvalcpre  34728  dihord4  34738  dihord6b  34740  dihmeetlem1N  34770  dihglblem3N  34775  dihmeetlem2N  34779  dihglbcpreN  34780  dihmeetcN  34782  dihmeetbclemN  34784  dihmeetlem4preN  34786  dihjatc1  34791  dihjatc2N  34792  dihjatc3  34793  dihmeetlem9N  34795  dihmeetlem13N  34799  dihmeetlem20N  34806  dih1dimatlem0  34808  mapdpglem24  35184  mapdpglem32  35185  baerlem3lem2  35190  baerlem5alem2  35191  baerlem5blem2  35192  mapdh9aOLDN  35271  hdmap14lem6  35356  mzpsubst  35502  pellexlem5  35590  pellex  35592  pell14qrexpclnn0  35625  pellfundex  35647  qirropth  35669  monotuz  35702  expmordi  35708  congtr  35728  congmul  35730  congsub  35733  mzpcong  35735  fzmaxdif  35744  jm2.15nn0  35771  idomsubgmo  35985  iunrelexpmin1  36213  iunrelexpmin2  36217  trclimalb2  36231  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem80  37933  lidldomn1  39522  rngccatidALTV  39592  coe1sclmulval  39780  lincdifsn  39820
  Copyright terms: Public domain W3C validator