Theorem simp2l 1087

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 1083	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl2l  1114  simpr2l  1120  simp12l  1174  simp22l  1180  simp32l  1186  funprgOLD  5941  fsnunf  6451  f1oiso2  6602  omeulem2  7663  uniinqs  7827  unxpdomlem3  8166  gruina  9640  dedekind  10200  addid2  10219  dmdcan  10735  xaddass  12079  xaddass2  12080  xlt2add  12090  xmulasslem3  12116  xadddi2  12127  xadddi2r  12128  expaddzlem  12903  expaddz  12904  expmulz  12906  expdiv  12911  modexp  12999  ccatopth2  13471  swrdco  13583  o1add  14344  o1mul  14345  o1sub  14346  fsumsplitsnun  14484  ntrivcvgmul  14634  prmexpb  15430  pcpremul  15548  pcdiv  15557  pcqmul  15558  pcqdiv  15562  4sqlem12  15660  f1ocpbllem  16184  ercpbl  16209  erlecpbl  16210  latjlej12  17067  latmlem12  17083  latj4  17101  latj4rot  17102  symgsssg  17887  symgfisg  17888  mndodcong  17961  cmn4  18212  ablsub4  18218  abladdsub4  18219  lsm4  18263  abvdom  18838  abvres  18839  abvtrivd  18840  lspsnvs  19114  lspsneu  19123  lspfixed  19128  lspexch  19129  lsmcv  19141  lspsolvlem  19142  coe1sclmulfv  19653  matvscacell  20242  m1detdiag  20403  cramerimplem3  20491  cnprest  21093  hausnei2  21157  isreg2  21181  cmpcld  21205  llyrest  21288  nllyrest  21289  elptr  21376  basqtop  21514  hausflimlem  21783  tmdgsum  21899  utop2nei  22054  trcfilu  22098  ssblps  22227  ssbl  22228  prdsxmslem2  22334  tgqioo  22603  metnrm  22665  bndth  22757  ncvspi  22956  ncvs1  22957  cph2ass  23013  lmmbr2  23057  iscau3  23076  bcthlem5  23125  ovolunlem2  23266  dvres2  23676  dvfsumlem2  23790  plyadd  23973  plymul  23974  coeeu  23981  coemullem  24006  aalioulem4  24090  mulcxp  24431  cxplea  24442  cxple2  24443  cxplt2  24444  cxpcn3lem  24488  angcan  24532  ang180lem5  24543  divsqrtsumlem  24706  logexprlim  24950  dchrvmasumlema  25189  dchrisum0lema  25203  logdivsum  25222  log2sumbnd  25233  abvcxp  25304  padicabv  25319  tghilberti2  25533  brbtwn2  25785  axcontlem4  25847  axcontlem8  25851  clwlkl1loop  26678  clwwlksel  26914  numclwwlkovf2exlem2  27212  chscllem4  28499  orngmul  29803  measxun2  30273  measun  30274  mbfmco2  30327  probun  30481  nolesgn2ores  31825  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem2  31855  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  scutbdaylt  31922  cgrcomim  32096  cgrcoml  32103  cgrcomr  32104  cgrdegen  32111  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  btwnouttr  32131  btwnexch  32132  btwndiff  32134  lineid  32190  idinside  32191  btwnconn1lem7  32200  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem12  32205  btwnconn1lem14  32207  btwnconn3  32210  midofsegid  32211  segcon2  32212  brsegle2  32216  btwnoutside  32232  outsideoftr  32236  outsideofeu  32238  linethru  32260  cnres2  33562  heibor  33620  lsmsat  34295  lkrlsp  34389  lkrlsp2  34390  lkrlsp3  34391  latm4  34520  omlspjN  34548  hlatj4  34660  4noncolr3  34739  4noncolr2  34740  4noncolr1  34741  athgt  34742  3dimlem3a  34746  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  3dim3  34755  1cvratex  34759  hlatexch4  34767  3atlem4  34772  atcvrlln2  34805  atcvrlln  34806  lplnnlelln  34829  lvoli2  34867  lvolnlelln  34870  lvolnlelpln  34871  4atlem11b  34894  4atlem12b  34897  2lplnja  34905  2lplnj  34906  dalemyeo  34918  dath2  35023  lncvrat  35068  cdlemblem  35079  cdlemb  35080  elpaddri  35088  padd4N  35126  llnmod2i2  35149  llnexchb2  35155  dalawlem1  35157  dalawlem2  35158  pclfinN  35186  osumcllem6N  35247  pexmidlem3N  35258  lhp2lt  35287  lhp2at0  35318  lhp2atnle  35319  lhp2atne  35320  lhp2at0nle  35321  lhp2at0ne  35322  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  lhple  35328  lhpat  35329  lhpat3  35332  ltrncoelN  35429  ltrncoat  35430  ltrncnv  35432  trlat  35456  trl0  35457  ltrnnidn  35461  trlnid  35466  cdlemd7  35491  cdleme0b  35499  cdleme0c  35500  cdleme0fN  35505  cdleme02N  35509  cdleme0ex1N  35510  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme8  35537  cdleme11a  35547  cdleme17c  35575  cdleme22gb  35581  cdlemeda  35585  cdleme20k  35607  cdleme21a  35613  cdleme21d  35618  cdleme22f2  35635  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme24  35640  cdleme28  35661  cdlemefrs32fva1  35689  cdlemefr32sn2aw  35692  cdlemefs32sn1aw  35702  cdleme41sn3a  35721  cdleme32fva  35725  cdleme32fva1  35726  cdleme35a  35736  cdleme35b  35738  cdleme35c  35739  cdleme35f  35742  cdleme39a  35753  cdleme42a  35759  cdleme42c  35760  cdleme42b  35766  cdleme42e  35767  cdleme42f  35768  cdleme42g  35769  cdleme42h  35770  cdleme43bN  35778  cdleme46f2g2  35781  cdleme17d2  35783  cdleme17d4  35785  cdleme48fv  35787  cdleme48fvg  35788  cdleme4gfv  35795  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46gfre  35820  cdleme48d  35823  cdlemeg49lebilem  35827  cdleme50trn2  35839  cdleme50ltrn  35845  cdleme  35848  cdlemf1  35849  cdlemf  35851  trlord  35857  ltrniotacnvval  35870  ltrniotavalbN  35872  cdlemg1cex  35876  cdlemg2dN  35878  cdlemg2ce  35880  cdlemg2fvlem  35882  cdlemg2idN  35884  cdlemg2kq  35890  cdlemg2l  35891  cdlemg2m  35892  cdlemg4b2  35898  cdlemg7fvN  35912  cdlemg8a  35915  cdlemg10bALTN  35924  cdlemg11aq  35926  cdlemg12d  35934  cdlemg13a  35939  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17a  35949  cdlemg17b  35950  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg31a  35985  cdlemg31b  35986  cdlemg31c  35987  ltrnco  36007  trlcoabs  36009  trlcoabs2N  36010  trlcocnvat  36012  trlconid  36013  trlcolem  36014  trlcone  36016  cdlemg42  36017  cdlemg43  36018  cdlemg46  36023  cdlemg47  36024  tendoeq1  36052  tendoco2  36056  tendoplco2  36067  tendopltp  36068  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  cdlemi  36108  cdlemk1  36119  cdlemk2  36120  cdlemk3  36121  cdlemk4  36122  cdlemk8  36126  cdlemk9  36127  cdlemk9bN  36128  cdlemk31  36184  cdlemk32  36185  cdlemk28-3  36196  cdlemk19u  36258  cdlemk56w  36261  tendoex  36263  erngdvlem4  36279  erngdvlem4-rN  36287  dia11N  36337  dib11N  36449  cdlemn6  36491  cdlemn7  36492  cdlemn8  36493  cdlemn9  36494  dihordlem6  36502  dihordlem7  36503  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord2pre  36514  dihord2pre2  36515  dihlsscpre  36523  dihvalcq2  36536  dihopelvalcpre  36537  dihord4  36547  dihord6b  36549  dihmeetlem1N  36579  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetcN  36591  dihmeetbclemN  36593  dihmeetlem4preN  36595  dihjatc1  36600  dihjatc2N  36601  dihjatc3  36602  dihmeetlem9N  36604  dihmeetlem13N  36608  dihmeetlem20N  36615  dih1dimatlem0  36617  mapdpglem24  36993  mapdpglem32  36994  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  mapdh9aOLDN  37080  hdmap14lem6  37165  mzpsubst  37311  pellexlem5  37397  pellex  37399  pell14qrexpclnn0  37430  pellfundex  37450  qirropth  37473  monotuz  37506  expmordi  37512  congtr  37532  congmul  37534  congsub  37537  mzpcong  37539  fzmaxdif  37548  jm2.15nn0  37570  idomsubgmo  37776  iunrelexpmin1  38000  iunrelexpmin2  38004  trclimalb2  38018  fourierdlem42  40366  fourierdlem48  40371  fourierdlem80  40403  smfaddlem1  40971  prmdvdsfmtnof1lem1  41496  uspgropssxp  41752  lidldomn1  41921  rngccatidALTV  41989  coe1sclmulval  42173  lincdifsn  42213