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

Theorem simp2l 981
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 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl2l  1008  simpr2l  1014  simp12l  1068  simp22l  1074  simp32l  1080  funprg  5317  fsnunf  5734  f1oiso2  5865  omeulem2  6597  unxpdomlem3  7085  gruina  8456  addid2  9011  dmdcan  9486  xaddass  10585  xaddass2  10586  xlt2add  10596  xmulasslem3  10622  xadddi2  10633  xadddi2r  10634  expaddzlem  11161  expaddz  11162  expmulz  11164  expdiv  11168  modexp  11252  ccatopth2  11479  o1add  12103  o1mul  12104  o1sub  12105  prmexpb  12812  pcpremul  12912  pcdiv  12921  pcqmul  12922  pcqdiv  12926  4sqlem12  13019  f1ocpbllem  13442  ercpbl  13467  erlecpbl  13468  latjlej12  14189  latmlem12  14205  latj4  14223  latj4rot  14224  mndodcong  14873  cmn4  15124  ablsub4  15130  abladdsub4  15131  lsm4  15168  abvdom  15619  abvres  15620  abvtrivd  15621  lspsnvs  15883  lspsneu  15892  lspfixed  15897  lspexch  15898  lsmcv  15910  lspsolvlem  15911  coe1sclmulfv  16375  cnprest  17033  hausnei2  17097  isreg2  17121  cmpcld  17145  llyrest  17227  nllyrest  17228  elptr  17284  basqtop  17418  hausflimlem  17690  tmdgsum  17794  ssbl  17987  prdsxmslem2  18091  tgqioo  18322  metnrm  18382  bndth  18472  cph2ass  18664  lmmbr2  18701  iscau3  18720  bcthlem5  18766  ovolunlem2  18873  dvres2  19278  dvfsumlem2  19390  plyadd  19615  plymul  19616  coeeu  19623  coemullem  19647  aalioulem4  19731  mulcxp  20048  cxplea  20059  cxple2  20060  cxplt2  20061  cxpcn3lem  20103  angcan  20116  ang180lem5  20127  divsqrsumlem  20290  logexprlim  20480  dchrvmasumlema  20665  dchrisum0lema  20679  logdivsum  20698  log2sumbnd  20709  abvcxp  20780  padicabv  20795  gxmodid  20962  chscllem4  22235  measxun  23554  mbfmco2  23585  dedekind  24097  nofulllem5  24431  brbtwn2  24605  axcontlem4  24667  axcontlem8  24671  cgrcomim  24684  cgrcoml  24691  cgrcomr  24692  cgrdegen  24699  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  btwnouttr  24719  btwnexch  24720  btwndiff  24722  lineid  24778  idinside  24779  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem12  24793  btwnconn1lem14  24795  btwnconn3  24798  midofsegid  24799  segcon2  24800  brsegle2  24804  btwnoutside  24820  outsideoftr  24824  outsideofeu  24826  linethru  24848  uninqs  25142  oriso  25317  islimrs3  25684  islimrs4  25685  icccon4  25805  imonclem  25916  ismonc  25917  rocatval  26062  clscnc  26113  cnres2  26586  heibor  26648  mzpsubst  26929  pellexlem5  27021  pellex  27023  pell14qrexpclnn0  27054  pellfundex  27074  qirropth  27096  monotuz  27129  expmordi  27135  congtr  27155  congmul  27157  congsub  27160  mzpcong  27162  fzmaxdif  27171  jm2.15nn0  27199  symgsssg  27511  symgfisg  27512  idomsubgmo  27617  lsmsat  29820  lkrlsp  29914  lkrlsp2  29915  lkrlsp3  29916  latm4  30045  omlspjN  30073  hlatj4  30185  4noncolr3  30264  4noncolr2  30265  4noncolr1  30266  athgt  30267  3dimlem3a  30271  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  3dim3  30280  1cvratex  30284  hlatexch4  30292  3atlem4  30297  atcvrlln2  30330  atcvrlln  30331  lplnnlelln  30354  lvoli2  30392  lvolnlelln  30395  lvolnlelpln  30396  4atlem11b  30419  4atlem12b  30422  2lplnja  30430  2lplnj  30431  dalemyeo  30443  dath2  30548  lncvrat  30593  cdlemblem  30604  cdlemb  30605  elpaddri  30613  padd4N  30651  llnmod2i2  30674  llnexchb2  30680  dalawlem1  30682  dalawlem2  30683  pclfinN  30711  osumcllem6N  30772  pexmidlem3N  30783  lhp2lt  30812  lhp2at0  30843  lhp2atnle  30844  lhp2atne  30845  lhp2at0nle  30846  lhp2at0ne  30847  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  lhple  30853  lhpat  30854  lhpat3  30857  ltrncoelN  30954  ltrncoat  30955  ltrncnv  30957  trlat  30980  trl0  30981  ltrnnidn  30985  trlnid  30990  cdlemd7  31015  cdleme0b  31023  cdleme0c  31024  cdleme0fN  31029  cdleme02N  31033  cdleme0ex1N  31034  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme8  31061  cdleme11a  31071  cdleme17c  31099  cdleme22gb  31105  cdlemeda  31109  cdleme20k  31130  cdleme21a  31136  cdleme21d  31141  cdleme22f2  31158  cdleme22g  31159  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme24  31163  cdleme28  31184  cdlemefrs32fva1  31212  cdlemefr32sn2aw  31215  cdlemefs32sn1aw  31225  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32fva1  31249  cdleme35a  31259  cdleme35b  31261  cdleme35c  31262  cdleme35f  31265  cdleme39a  31276  cdleme42a  31282  cdleme42c  31283  cdleme42b  31289  cdleme42e  31290  cdleme42f  31291  cdleme42g  31292  cdleme42h  31293  cdleme43bN  31301  cdleme46f2g2  31304  cdleme17d2  31306  cdleme17d4  31308  cdleme48fv  31310  cdleme48fvg  31311  cdleme4gfv  31318  cdlemeg46c  31324  cdlemeg46nlpq  31328  cdlemeg46gfre  31343  cdleme48d  31346  cdlemeg49lebilem  31350  cdleme50trn2  31362  cdleme50ltrn  31368  cdleme  31371  cdlemf1  31372  cdlemf  31374  trlord  31380  ltrniotacnvval  31393  ltrniotavalbN  31395  cdlemg1cex  31399  cdlemg2dN  31401  cdlemg2ce  31403  cdlemg2fvlem  31405  cdlemg2idN  31407  cdlemg2kq  31413  cdlemg2l  31414  cdlemg2m  31415  cdlemg4b2  31421  cdlemg7fvN  31435  cdlemg8a  31438  cdlemg10bALTN  31447  cdlemg11aq  31449  cdlemg12d  31457  cdlemg13a  31462  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17a  31472  cdlemg17b  31473  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg31a  31508  cdlemg31b  31509  cdlemg31c  31510  ltrnco  31530  trlcoabs  31532  trlcoabs2N  31533  trlcocnvat  31535  trlconid  31536  trlcolem  31537  trlcone  31539  cdlemg42  31540  cdlemg43  31541  cdlemg46  31546  cdlemg47  31547  tendoeq1  31575  tendoco2  31579  tendoplco2  31590  tendopltp  31591  cdlemh1  31626  cdlemh2  31627  cdlemi1  31629  cdlemi  31631  cdlemk1  31642  cdlemk2  31643  cdlemk3  31644  cdlemk4  31645  cdlemk8  31649  cdlemk9  31650  cdlemk9bN  31651  cdlemk31  31707  cdlemk32  31708  cdlemk28-3  31719  cdlemk19u  31781  cdlemk56w  31784  tendoex  31786  erngdvlem4  31802  erngdvlem4-rN  31810  dia11N  31860  dib11N  31972  cdlemn6  32014  cdlemn7  32015  cdlemn8  32016  cdlemn9  32017  dihordlem6  32025  dihordlem7  32026  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord2pre  32037  dihord2pre2  32038  dihlsscpre  32046  dihvalcq2  32059  dihopelvalcpre  32060  dihord4  32070  dihord6b  32072  dihmeetlem1N  32102  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbclemN  32116  dihmeetlem4preN  32118  dihjatc1  32123  dihjatc2N  32124  dihjatc3  32125  dihmeetlem9N  32127  dihmeetlem13N  32131  dihmeetlem20N  32138  dih1dimatlem0  32140  mapdpglem24  32516  mapdpglem32  32517  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  mapdh9aOLDN  32603  hdmap14lem6  32688
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