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

Theorem simp3l 1016
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 457 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1011 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  simpl3l  1043  simpr3l  1049  simp13l  1103  simp23l  1109  simp33l  1115  disjss3  4296  tfisi  6474  tfrlem5  6844  omeulem1  7026  omeulem2  7027  uniinqs  7185  elfiun  7685  tcrank  8096  isfin2-2  8493  konigthlem  8737  gruen  8984  addid2  9557  mulcan  9978  mulcan2  9979  divass  10017  divdir  10022  div11  10025  divcan5  10038  ltmul1  10184  ltdiv1  10198  ltmuldiv  10207  lediv2  10227  xaddass2  11218  xlt2add  11228  xmulasslem3  11254  xadddi2  11265  expaddz  11913  expmulz  11915  resqrcl  12748  o1add  13096  o1mul  13097  o1sub  13098  dvdsadd2b  13580  dvdsgcd  13732  rpexp12i  13813  pythagtriplem3  13890  pcpremul  13915  pceu  13918  pcqmul  13925  pcqdiv  13929  f1ocpbllem  14467  funcoppc  14790  funcres  14811  catcisolem  14979  1stfcl  15012  2ndfcl  15013  prfcl  15018  evlfcl  15037  curf1cl  15043  curfcl  15047  hofcl  15074  latjlej12  15242  latmlem12  15258  latj4  15276  latj4rot  15277  symgsssg  15978  symgfisg  15979  psgnunilem4  16008  odcong  16057  cmn4  16301  ablsub4  16307  abladdsub4  16308  lsm4  16347  abvdom  16928  abvres  16929  abvtrivd  16930  lspsolvlem  17228  lbsextlem2  17245  frlmbas3  18206  marrepeval  18379  ma1repveval  18387  submaeval  18398  mdetunilem3  18425  mdetuni0  18432  mdetmul  18434  minmar1eval  18460  nllyrest  19095  hausflimlem  19557  tsmsxp  19734  psmetlecl  19896  xmetlecl  19926  prdsxmetlem  19948  bndth  20535  cph2ass  20736  iscau3  20794  dvres2  21392  coemullem  21722  vieta1  21783  aalioulem4  21806  cxpcn3lem  22190  angcan  22203  dchrvmasumlema  22754  logdivsum  22787  abvcxp  22869  padicabv  22884  ax5seglem3  23182  ax5seglem6  23185  axpasch  23192  axeuclid  23214  axcontlem4  23218  axcontlem8  23222  gxneg  23758  gxsuc  23764  gxmodid  23771  adjlnop  25495  xreceu  26102  orngmul  26276  rhmdvd  26294  measvunilem  26631  measvunilem0  26632  measres  26641  subdivcomb1  27389  subdivcomb2  27390  cgrcomim  28025  cgrcoml  28032  cgrcomr  28033  cgrdegen  28040  segconeu  28047  btwnintr  28055  btwnexch3  28056  btwnouttr2  28058  btwnouttr  28060  btwnexch  28061  trisegint  28064  lineext  28112  linecgr  28117  lineid  28119  idinside  28120  btwnconn1lem3  28125  btwnconn1lem4  28126  btwnconn1lem7  28129  btwnconn1lem14  28136  btwnconn2  28138  midofsegid  28140  btwnoutside  28161  outsideoftr  28165  lineunray  28183  lineelsb2  28184  cnres2  28667  heibor  28725  mzpsubst  29090  pellex  29181  pellfundex  29232  pellfund14gap  29233  qirropth  29254  rmxypos  29295  congmul  29315  congsub  29318  mzpcong  29320  coprmdvdsb  29335  jm2.15nn0  29357  jm2.16nn0  29358  rpnnen3lem  29385  idomsubgmo  29568  stoweidlem57  29857  clwwlknimp  30444  bnj1128  31986  lsmcv2  32679  lcvat  32680  lcvexchlem4  32687  lcvexchlem5  32688  lfladd  32716  lflsub  32717  lflmul  32718  lshpkrlem4  32763  latm4  32883  omlmod1i2N  32910  cvlatexch3  32988  cvlsupr7  32998  hlatj4  33023  hlrelat3  33061  cvrval3  33062  atcvrj1  33080  atlelt  33087  2atlt  33088  2atjm  33094  3noncolr2  33098  athgt  33105  3dimlem2  33108  3dimlem4  33113  3dimlem4OLDN  33114  3dim3  33118  1cvratex  33122  ps-1  33126  ps-2  33127  hlatexch3N  33129  llnle  33167  atcvrlln2  33168  atcvrlln  33169  lplni2  33186  lplnle  33189  lplnnle2at  33190  llncvrlpln2  33206  lplnexllnN  33213  2llnmeqat  33220  lvolnle3at  33231  4atlem0ae  33243  lplncvrlvol2  33264  lnjatN  33429  lncvrat  33431  cdlemblem  33442  elpaddri  33451  paddasslem2  33470  paddasslem16  33484  padd4N  33489  hlmod1i  33505  dalawlem2  33521  pclfinN  33549  pexmidlem4N  33622  pl42lem1N  33628  lhp2lt  33650  lhpexle1  33657  lhpexle2lem  33658  lhpj1  33671  lhpmcvr5N  33676  lhp2at0  33681  lhp2atnle  33682  lhp2at0nle  33684  lhple  33691  lhpat  33692  lhpat4N  33693  4atexlempnq  33704  4atexlem7  33724  4atex  33725  ltrn11  33775  ltrnle  33778  ltrnm  33780  ltrnj  33781  ltrncvr  33782  ltrnel  33788  ltrncnvel  33791  ltrncnv  33795  ltrnmw  33800  trlval2  33812  trlcnv  33814  trljat1  33815  trljat2  33816  trlat  33818  trl0  33819  trlnidat  33822  trlnid  33828  cdlemc1  33840  cdlemc2  33841  cdlemc5  33844  cdlemd2  33848  cdlemd7  33853  cdlemd8  33854  cdlemd9  33855  cdleme0e  33866  cdleme3g  33883  cdleme3h  33884  cdleme3  33886  cdleme5  33889  cdleme10  33903  cdleme11a  33909  cdleme11c  33910  cdleme11h  33915  cdleme11j  33916  cdleme0nex  33939  cdleme18a  33940  cdleme18b  33941  cdleme22gb  33943  cdleme20zN  33950  cdleme20y  33951  cdleme20c  33960  cdleme20k  33968  cdleme21a  33974  cdleme21b  33975  cdleme21c  33976  cdleme21h  33983  cdleme22b  33990  cdleme22d  33992  cdleme22f  33995  cdleme25a  34002  cdleme25c  34004  cdleme25dN  34005  cdleme26ee  34009  cdleme30a  34027  cdlemefr29bpre0N  34055  cdlemefr29clN  34056  cdlemefr32fvaN  34058  cdlemefr32fva1  34059  cdlemefs29bpre0N  34065  cdlemefs29bpre1N  34066  cdlemefs29cpre1N  34067  cdlemefs29clN  34068  cdleme43fsv1snlem  34069  cdlemefs32fvaN  34071  cdlemefs32fva1  34072  cdlemefs31fv1  34073  cdleme36a  34109  cdleme39a  34114  cdleme42a  34120  cdleme42c  34121  cdleme17d3  34145  cdleme48fv  34148  cdleme48bw  34151  cdleme48b  34152  cdlemeg46rgv  34177  cdlemeg46req  34178  cdlemeg46gfv  34179  cdleme48d  34184  cdleme50trn2a  34199  cdleme50trn2  34200  cdleme50ltrn  34206  cdlemf1  34210  cdlemf  34212  trlord  34218  cdlemg2dN  34239  cdlemg2fvlem  34243  cdlemg2l  34252  cdlemg7fvbwN  34256  cdlemg7aN  34274  cdlemg10bALTN  34285  cdlemg10c  34288  cdlemg17a  34310  cdlemg17dALTN  34313  cdlemg31b0a  34344  cdlemg31a  34346  cdlemg31b  34347  cdlemg34  34361  cdlemg36  34363  ltrnco  34368  trlcoabs2N  34371  trlcolem  34375  cdlemg48  34386  tgrpov  34397  tendoco2  34417  tendoplco2  34428  cdlemh1  34464  cdlemi1  34467  cdlemi2  34468  cdlemj3  34472  tendoid0  34474  cdlemk1  34480  cdlemk2  34481  cdlemk4  34483  cdlemk8  34487  cdlemk9  34488  cdlemk9bN  34489  cdlemk10  34492  cdlemk26b-3  34554  cdlemk26-3  34555  cdlemk28-3  34557  cdlemk37  34563  cdlemk39  34565  cdlemkfid1N  34570  cdlemkid1  34571  cdlemky  34575  cdlemkyu  34576  cdlemk19ylem  34579  cdlemk19xlem  34591  cdlemk11t  34595  cdlemk51  34602  cdlemkyyN  34611  cdleml6  34630  cdleml7  34631  cdleml8  34632  cdleml9  34633  erngdvlem4  34640  erngdvlem4-rN  34648  tendospcanN  34673  dia11N  34698  cdlemm10N  34768  dib11N  34810  dicvaddcl  34840  dicvscacl  34841  cdlemn6  34852  dihvalcq2  34897  dihopelvalcpre  34898  dihord6b  34910  dihord5apre  34912  dihmeetlem1N  34940  dihmeetlem2N  34949  dihglbcpreN  34950  dihjatc1  34961  dihmeetlem20N  34976  dih1dimatlem0  34978  dihatlat  34984  dihglblem6  34990  dochexmidlem4  35113  mapdpglem32  35355  mapdh8ad  35429  mapdh9aOLDN  35441  hdmap11lem2  35495  hdmap14lem6  35526
  Copyright terms: Public domain W3C validator