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

Theorem simp3l 985
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 444 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl3l  1012  simpr3l  1018  simp13l  1072  simp23l  1078  simp33l  1084  disjss3  4203  tfisi  4829  omeulem1  6816  omeulem2  6817  uniinqs  6975  elfiun  7426  tcrank  7797  isfin2-2  8188  konigthlem  8432  gruen  8676  addid2  9238  mulcan  9648  mulcan2  9649  divass  9685  divdir  9690  div11  9693  divcan5  9705  ltmul1  9849  ltdiv1  9863  ltmuldiv  9869  lediv2  9889  xaddass2  10818  xlt2add  10828  xmulasslem3  10854  xadddi2  10865  expaddz  11412  expmulz  11414  resqrcl  12047  o1add  12395  o1mul  12396  o1sub  12397  dvdsadd2b  12880  dvdsgcd  13031  rpexp12i  13110  pythagtriplem3  13180  pcpremul  13205  pceu  13208  pcqmul  13215  pcqdiv  13219  f1ocpbllem  13737  funcoppc  14060  funcres  14081  catcisolem  14249  1stfcl  14282  2ndfcl  14283  prfcl  14288  evlfcl  14307  curf1cl  14313  curfcl  14317  hofcl  14344  latjlej12  14484  latmlem12  14500  latj4  14518  latj4rot  14519  odcong  15175  cmn4  15419  ablsub4  15425  abladdsub4  15426  lsm4  15463  abvdom  15914  abvres  15915  abvtrivd  15916  lspsolvlem  16202  lbsextlem2  16219  nllyrest  17537  hausflimlem  17999  tsmsxp  18172  psmetlecl  18334  xmetlecl  18364  prdsxmetlem  18386  bndth  18971  cph2ass  19163  iscau3  19219  dvres2  19787  coemullem  20156  vieta1  20217  aalioulem4  20240  cxpcn3lem  20619  angcan  20632  dchrvmasumlema  21182  logdivsum  21215  abvcxp  21297  padicabv  21312  gxneg  21842  gxsuc  21848  gxmodid  21855  adjlnop  23577  xreceu  24156  rhmdvd  24247  measvunilem  24554  measvunilem0  24555  measres  24564  subdivcomb1  25183  subdivcomb2  25184  ax5seglem3  25818  ax5seglem6  25821  axpasch  25828  axeuclid  25850  axcontlem4  25854  axcontlem8  25858  cgrcomim  25871  cgrcoml  25878  cgrcomr  25879  cgrdegen  25886  segconeu  25893  btwnintr  25901  btwnexch3  25902  btwnouttr2  25904  btwnouttr  25906  btwnexch  25907  trisegint  25910  lineext  25958  linecgr  25963  lineid  25965  idinside  25966  btwnconn1lem3  25971  btwnconn1lem4  25972  btwnconn1lem7  25975  btwnconn1lem14  25982  btwnconn2  25984  midofsegid  25986  btwnoutside  26007  outsideoftr  26011  lineunray  26029  lineelsb2  26030  cnres2  26409  heibor  26467  mzpsubst  26742  pellex  26835  pellfundex  26886  pellfund14gap  26887  qirropth  26908  rmxypos  26949  congmul  26969  congsub  26972  mzpcong  26974  coprmdvdsb  26989  jm2.15nn0  27011  jm2.16nn0  27012  rpnnen3lem  27039  symgsssg  27323  symgfisg  27324  psgnunilem4  27335  idomsubgmo  27429  stoweidlem57  27720  bnj1128  29213  lsmcv2  29666  lcvat  29667  lcvexchlem4  29674  lcvexchlem5  29675  lfladd  29703  lflsub  29704  lflmul  29705  lshpkrlem4  29750  latm4  29870  omlmod1i2N  29897  cvlatexch3  29975  cvlsupr7  29985  hlatj4  30010  hlrelat3  30048  cvrval3  30049  atcvrj1  30067  atlelt  30074  2atlt  30075  2atjm  30081  3noncolr2  30085  athgt  30092  3dimlem2  30095  3dimlem4  30100  3dimlem4OLDN  30101  3dim3  30105  1cvratex  30109  ps-1  30113  ps-2  30114  hlatexch3N  30116  llnle  30154  atcvrlln2  30155  atcvrlln  30156  lplni2  30173  lplnle  30176  lplnnle2at  30177  llncvrlpln2  30193  lplnexllnN  30200  2llnmeqat  30207  lvolnle3at  30218  4atlem0ae  30230  lplncvrlvol2  30251  lnjatN  30416  lncvrat  30418  cdlemblem  30429  elpaddri  30438  paddasslem2  30457  paddasslem16  30471  padd4N  30476  hlmod1i  30492  dalawlem2  30508  pclfinN  30536  pexmidlem4N  30609  pl42lem1N  30615  lhp2lt  30637  lhpexle1  30644  lhpexle2lem  30645  lhpj1  30658  lhpmcvr5N  30663  lhp2at0  30668  lhp2atnle  30669  lhp2at0nle  30671  lhple  30678  lhpat  30679  lhpat4N  30680  4atexlempnq  30691  4atexlem7  30711  4atex  30712  ltrn11  30762  ltrnle  30765  ltrnm  30767  ltrnj  30768  ltrncvr  30769  ltrnel  30775  ltrncnvel  30778  ltrncnv  30782  ltrnmw  30787  trlval2  30799  trlcnv  30801  trljat1  30802  trljat2  30803  trlat  30805  trl0  30806  trlnidat  30809  trlnid  30815  cdlemc1  30827  cdlemc2  30828  cdlemc5  30831  cdlemd2  30835  cdlemd7  30840  cdlemd8  30841  cdlemd9  30842  cdleme0e  30853  cdleme3g  30870  cdleme3h  30871  cdleme3  30873  cdleme5  30876  cdleme10  30890  cdleme11a  30896  cdleme11c  30897  cdleme11h  30902  cdleme11j  30903  cdleme0nex  30926  cdleme18a  30927  cdleme18b  30928  cdleme22gb  30930  cdleme20zN  30937  cdleme20y  30938  cdleme20c  30947  cdleme20k  30955  cdleme21a  30961  cdleme21b  30962  cdleme21c  30963  cdleme21h  30970  cdleme22b  30977  cdleme22d  30979  cdleme22f  30982  cdleme25a  30989  cdleme25c  30991  cdleme25dN  30992  cdleme26ee  30996  cdleme30a  31014  cdlemefr29bpre0N  31042  cdlemefr29clN  31043  cdlemefr32fvaN  31045  cdlemefr32fva1  31046  cdlemefs29bpre0N  31052  cdlemefs29bpre1N  31053  cdlemefs29cpre1N  31054  cdlemefs29clN  31055  cdleme43fsv1snlem  31056  cdlemefs32fvaN  31058  cdlemefs32fva1  31059  cdlemefs31fv1  31060  cdleme36a  31096  cdleme39a  31101  cdleme42a  31107  cdleme42c  31108  cdleme17d3  31132  cdleme48fv  31135  cdleme48bw  31138  cdleme48b  31139  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemeg46gfv  31166  cdleme48d  31171  cdleme50trn2a  31186  cdleme50trn2  31187  cdleme50ltrn  31193  cdlemf1  31197  cdlemf  31199  trlord  31205  cdlemg2dN  31226  cdlemg2fvlem  31230  cdlemg2l  31239  cdlemg7fvbwN  31243  cdlemg7aN  31261  cdlemg10bALTN  31272  cdlemg10c  31275  cdlemg17a  31297  cdlemg17dALTN  31300  cdlemg31b0a  31331  cdlemg31a  31333  cdlemg31b  31334  cdlemg34  31348  cdlemg36  31350  ltrnco  31355  trlcoabs2N  31358  trlcolem  31362  cdlemg48  31373  tgrpov  31384  tendoco2  31404  tendoplco2  31415  cdlemh1  31451  cdlemi1  31454  cdlemi2  31455  cdlemj3  31459  tendoid0  31461  cdlemk1  31467  cdlemk2  31468  cdlemk4  31470  cdlemk8  31474  cdlemk9  31475  cdlemk9bN  31476  cdlemk10  31479  cdlemk26b-3  31541  cdlemk26-3  31542  cdlemk28-3  31544  cdlemk37  31550  cdlemk39  31552  cdlemkfid1N  31557  cdlemkid1  31558  cdlemky  31562  cdlemkyu  31563  cdlemk19ylem  31566  cdlemk19xlem  31578  cdlemk11t  31582  cdlemk51  31589  cdlemkyyN  31598  cdleml6  31617  cdleml7  31618  cdleml8  31619  cdleml9  31620  erngdvlem4  31627  erngdvlem4-rN  31635  tendospcanN  31660  dia11N  31685  cdlemm10N  31755  dib11N  31797  dicvaddcl  31827  dicvscacl  31828  cdlemn6  31839  dihvalcq2  31884  dihopelvalcpre  31885  dihord6b  31897  dihord5apre  31899  dihmeetlem1N  31927  dihmeetlem2N  31936  dihglbcpreN  31937  dihjatc1  31948  dihmeetlem20N  31963  dih1dimatlem0  31965  dihatlat  31971  dihglblem6  31977  dochexmidlem4  32100  mapdpglem32  32342  mapdh8ad  32416  mapdh9aOLDN  32428  hdmap11lem2  32482  hdmap14lem6  32513
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