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

Theorem simp3r 984
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3r  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl3r  1011  simpr3r  1017  simp13r  1071  simp23r  1077  simp33r  1083  disjss3  4024  tfisi  4651  f1oiso2  5851  omeulem1  6582  omeulem2  6583  elfiun  7185  isfin2-2  7947  addid2  8997  mulcan  9407  mulcan2  9408  divass  9444  divdir  9449  div11  9452  ltdiv1  9622  ltmuldiv  9628  lediv2  9648  xaddass2  10572  xlt2add  10582  expaddz  11148  expmulz  11150  resqrex  11738  resqrcl  11741  o1add  12089  o1mul  12090  o1sub  12091  dvdsgcd  12724  rpexp12i  12803  pythagtriplem4  12874  pythagtriplem11  12880  pythagtriplem13  12882  pcpremul  12898  pceu  12901  pcqmul  12908  pcqdiv  12912  f1ocpbllem  13428  funcoppc  13751  funcres  13772  catcisolem  13940  1stfcl  13973  2ndfcl  13974  prfcl  13979  evlfcl  13998  curf1cl  14004  curfcl  14008  hofcl  14035  latjlej12  14175  latmlem12  14191  latj4  14209  latj4rot  14210  odcong  14866  cmn4  15110  ablsub4  15116  abladdsub4  15117  lsm4  15154  abvdom  15605  abvtrivd  15607  lspsolvlem  15897  lbsextlem2  15914  hausflimlem  17676  xmetlecl  17913  prdsxmetlem  17934  xblcntr  17965  bndth  18458  cph2ass  18650  iscau3  18706  dvres2  19264  coemullem  19633  vieta1  19694  aalioulem4  19717  cxpcn3lem  20089  angcan  20102  divsqrsumlem  20276  dchrmusumlema  20644  dchrvmasumlema  20651  dchrisum0lema  20665  logdivsum  20684  padicabv  20781  gxnval  20929  gxnn0mul  20946  adjlnop  22668  xreceu  23107  measvunilem  23542  measvuni  23544  ax5seglem3  24561  ax5seglem6  24564  axpasch  24571  axeuclid  24593  axcontlem4  24597  axcontlem8  24601  cgrcomim  24614  cgrcoml  24621  cgrcomr  24622  cgrdegen  24629  segconeu  24636  btwnintr  24644  btwnexch3  24645  btwnouttr2  24647  btwnouttr  24649  btwnexch  24650  ifscgr  24669  lineext  24701  linecgr  24706  lineid  24708  idinside  24709  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem14  24725  btwnconn2  24727  btwnconn3  24728  midofsegid  24729  btwnoutside  24750  outsideoftr  24754  lineunray  24772  lineelsb2  24773  itg2addnclem  24933  itg2addnc  24935  infxpg  25106  valvalcurfn  25217  prltub  25271  mulinvsca  25491  conttnf2  25573  prdnei  25584  mulmulvec  25698  distsava  25700  cmpmorass  25977  lppotos  26155  cnres2  26494  heibor  26556  mzpmfp  26836  mzpsubst  26837  pellex  26931  pellfundex  26982  pellfund14gap  26983  qirropth  27004  rmxypos  27045  congmul  27065  congsub  27068  mzpcong  27070  coprmdvdsb  27085  jm2.15nn0  27107  jm2.16nn0  27108  rpnnen3lem  27135  symgsssg  27419  symgfisg  27420  idomsubgmo  27525  bnj1128  29093  lsmcv2  29292  lcvat  29293  lcvexchlem4  29300  lcvexchlem5  29301  lfladd  29329  lflsub  29330  lflmul  29331  lshpkrlem4  29376  latm4  29496  omlmod1i2N  29523  cvlsupr7  29611  cvlsupr8  29612  hlatj4  29636  hlrelat3  29674  cvrval3  29675  atcvrj1  29693  atlelt  29700  2atlt  29701  2atjm  29707  3noncolr2  29711  athgt  29718  3dimlem2  29721  3dimlem4OLDN  29727  1cvratex  29735  ps-1  29739  ps-2  29740  hlatexch3N  29742  llnle  29780  atcvrlln2  29781  atcvrlln  29782  lplni2  29799  lplnle  29802  lplnnle2at  29803  lplnnlelln  29805  llncvrlpln2  29819  2llnmeqat  29833  lvolnle3at  29844  lvolnlelln  29846  4atlem0ae  29856  lneq2at  30040  lnjatN  30042  lncvrat  30044  2lnat  30046  elpaddri  30064  paddasslem2  30083  padd4N  30102  hlmod1i  30118  llnexchb2  30131  dalawlem2  30134  pclfinN  30162  pexmidlem4N  30235  pl42lem1N  30241  lhp2lt  30263  lhpexle1  30270  lhpexle2lem  30271  lhpj1  30284  lhpmcvr5N  30289  lhp2at0  30294  lhp2at0nle  30297  lhple  30304  lhpat  30305  lhpat4N  30306  4atexlemnslpq  30318  4atexlem7  30337  ltrn11  30388  ltrnle  30391  ltrnm  30393  ltrnj  30394  ltrncvr  30395  ltrnel  30401  ltrncnvel  30404  ltrncnv  30408  ltrnmw  30413  trlat  30431  trl0  30432  trlnidat  30435  trlnid  30441  ltrnatlw  30445  trlne  30447  trlval4  30450  cdlemc5  30457  cdlemd2  30461  cdlemd7  30466  cdlemd8  30467  cdlemd9  30468  cdleme0c  30475  cdleme0e  30479  cdleme0fN  30480  cdleme3g  30496  cdleme3h  30497  cdleme5  30502  cdleme11c  30523  cdleme11h  30528  cdleme11j  30529  cdleme11k  30530  cdleme0nex  30552  cdleme18a  30553  cdleme22gb  30556  cdleme20zN  30563  cdleme20y  30564  cdleme20c  30573  cdleme20k  30581  cdleme21a  30587  cdleme21b  30588  cdleme21c  30589  cdleme21ct  30591  cdleme21h  30596  cdleme22d  30605  cdleme22f  30608  cdleme26ee  30622  cdleme30a  30640  cdlemefs45eN  30693  cdleme36a  30722  cdleme36m  30723  cdleme39a  30727  cdleme42b  30740  cdleme43dN  30754  cdlemeg47rv2  30772  cdlemeg46sfg  30782  cdlemeg46rjgN  30784  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfv  30792  cdleme48d  30797  cdleme50ltrn  30819  cdlemf1  30823  cdlemf  30825  cdlemg2dN  30852  cdlemg2fvlem  30856  cdlemg2l  30865  cdlemg7fvbwN  30869  cdlemg7aN  30887  cdlemg10c  30901  cdlemg17a  30923  cdlemg17dALTN  30926  cdlemg18a  30940  cdlemg18b  30941  cdlemg31b0a  30957  cdlemg31a  30959  cdlemg31b  30960  ltrnco  30981  cdlemg48  30999  tgrpov  31010  tendoco2  31030  tendoplco2  31041  cdlemh1  31077  cdlemk1  31093  cdlemk26b-3  31167  cdlemk27-3  31169  cdlemk28-3  31170  cdlemk34  31172  cdlemkfid1N  31183  cdlemkid3N  31195  cdlemkid4  31196  cdlemk35s-id  31200  cdlemk39s-id  31202  cdlemk51  31215  tendospcanN  31286  cdlemm10N  31381  dicvaddcl  31453  dicvscacl  31454  cdlemn6  31465  dihvalcq2  31510  dihord6b  31523  dihord5apre  31525  dihglbcpreN  31563  dihjatc1  31574  dihmeetlem20N  31589  dih1dimatlem0  31591  dihglblem6  31603  dochexmidlem4  31726  mapdpglem32  31968  mapdh8ad  32042  mapdh9aOLDN  32054  hdmap11lem2  32108  hdmap14lem6  32139
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