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  4023  tfisi  4648  f1oiso2  5811  omeulem1  6576  omeulem2  6577  elfiun  7179  isfin2-2  7941  addid2  8991  mulcan  9401  mulcan2  9402  divass  9438  divdir  9443  div11  9446  ltdiv1  9616  ltmuldiv  9622  lediv2  9642  xaddass2  10566  xlt2add  10576  expaddz  11142  expmulz  11144  resqrex  11732  resqrcl  11735  o1add  12083  o1mul  12084  o1sub  12085  dvdsgcd  12718  rpexp12i  12797  pythagtriplem4  12868  pythagtriplem11  12874  pythagtriplem13  12876  pcpremul  12892  pceu  12895  pcqmul  12902  pcqdiv  12906  f1ocpbllem  13422  funcoppc  13745  funcres  13766  catcisolem  13934  1stfcl  13967  2ndfcl  13968  prfcl  13973  evlfcl  13992  curf1cl  13998  curfcl  14002  hofcl  14029  latjlej12  14169  latmlem12  14185  latj4  14203  latj4rot  14204  odcong  14860  cmn4  15104  ablsub4  15110  abladdsub4  15111  lsm4  15148  abvdom  15599  abvtrivd  15601  lspsolvlem  15891  lbsextlem2  15908  hausflimlem  17670  xmetlecl  17907  prdsxmetlem  17928  xblcntr  17959  bndth  18452  cph2ass  18644  iscau3  18700  dvres2  19258  coemullem  19627  vieta1  19688  aalioulem4  19711  cxpcn3lem  20083  angcan  20096  divsqrsumlem  20270  dchrmusumlema  20638  dchrvmasumlema  20645  dchrisum0lema  20659  logdivsum  20678  padicabv  20775  gxnval  20921  gxnn0mul  20938  adjlnop  22662  axfelem17  23766  ax5seglem3  23969  ax5seglem6  23972  axpasch  23979  axeuclid  24001  axcontlem4  24005  axcontlem8  24009  cgrcomim  24022  cgrcoml  24029  cgrcomr  24030  cgrdegen  24037  segconeu  24044  btwnintr  24052  btwnexch3  24053  btwnouttr2  24055  btwnouttr  24057  btwnexch  24058  ifscgr  24077  lineext  24109  linecgr  24114  lineid  24116  idinside  24117  btwnconn1lem3  24122  btwnconn1lem4  24123  btwnconn1lem14  24133  btwnconn2  24135  btwnconn3  24136  midofsegid  24137  btwnoutside  24158  outsideoftr  24162  lineunray  24180  lineelsb2  24181  infxpg  24505  valvalcurfn  24617  prltub  24671  mulinvsca  24891  conttnf2  24973  prdnei  24984  mulmulvec  25098  distsava  25100  cmpmorass  25377  lppotos  25555  cnres2  25894  heibor  25956  mzpmfp  26236  mzpsubst  26237  pellex  26331  pellfundex  26382  pellfund14gap  26383  qirropth  26404  rmxypos  26445  congmul  26465  congsub  26468  mzpcong  26470  coprmdvdsb  26485  jm2.15nn0  26507  jm2.16nn0  26508  rpnnen3lem  26535  symgsssg  26819  symgfisg  26820  idomsubgmo  26925  bnj1128  28299  lsmcv2  28498  lcvat  28499  lcvexchlem4  28506  lcvexchlem5  28507  lfladd  28535  lflsub  28536  lflmul  28537  lshpkrlem4  28582  latm4  28702  omlmod1i2N  28729  cvlsupr7  28817  cvlsupr8  28818  hlatj4  28842  hlrelat3  28880  cvrval3  28881  atcvrj1  28899  atlelt  28906  2atlt  28907  2atjm  28913  3noncolr2  28917  athgt  28924  3dimlem2  28927  3dimlem4OLDN  28933  1cvratex  28941  ps-1  28945  ps-2  28946  hlatexch3N  28948  llnle  28986  atcvrlln2  28987  atcvrlln  28988  lplni2  29005  lplnle  29008  lplnnle2at  29009  lplnnlelln  29011  llncvrlpln2  29025  2llnmeqat  29039  lvolnle3at  29050  lvolnlelln  29052  4atlem0ae  29062  lneq2at  29246  lnjatN  29248  lncvrat  29250  2lnat  29252  elpaddri  29270  paddasslem2  29289  padd4N  29308  hlmod1i  29324  llnexchb2  29337  dalawlem2  29340  pclfinN  29368  pexmidlem4N  29441  pl42lem1N  29447  lhp2lt  29469  lhpexle1  29476  lhpexle2lem  29477  lhpj1  29490  lhpmcvr5N  29495  lhp2at0  29500  lhp2at0nle  29503  lhple  29510  lhpat  29511  lhpat4N  29512  4atexlemnslpq  29524  4atexlem7  29543  ltrn11  29594  ltrnle  29597  ltrnm  29599  ltrnj  29600  ltrncvr  29601  ltrnel  29607  ltrncnvel  29610  ltrncnv  29614  ltrnmw  29619  trlat  29637  trl0  29638  trlnidat  29641  trlnid  29647  ltrnatlw  29651  trlne  29653  trlval4  29656  cdlemc5  29663  cdlemd2  29667  cdlemd7  29672  cdlemd8  29673  cdlemd9  29674  cdleme0c  29681  cdleme0e  29685  cdleme0fN  29686  cdleme3g  29702  cdleme3h  29703  cdleme5  29708  cdleme11c  29729  cdleme11h  29734  cdleme11j  29735  cdleme11k  29736  cdleme0nex  29758  cdleme18a  29759  cdleme22gb  29762  cdleme20zN  29769  cdleme20y  29770  cdleme20c  29779  cdleme20k  29787  cdleme21a  29793  cdleme21b  29794  cdleme21c  29795  cdleme21ct  29797  cdleme21h  29802  cdleme22d  29811  cdleme22f  29814  cdleme26ee  29828  cdleme30a  29846  cdlemefs45eN  29899  cdleme36a  29928  cdleme36m  29929  cdleme39a  29933  cdleme42b  29946  cdleme43dN  29960  cdlemeg47rv2  29978  cdlemeg46sfg  29988  cdlemeg46rjgN  29990  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemeg46gfv  29998  cdleme48d  30003  cdleme50ltrn  30025  cdlemf1  30029  cdlemf  30031  cdlemg2dN  30058  cdlemg2fvlem  30062  cdlemg2l  30071  cdlemg7fvbwN  30075  cdlemg7aN  30093  cdlemg10c  30107  cdlemg17a  30129  cdlemg17dALTN  30132  cdlemg18a  30146  cdlemg18b  30147  cdlemg31b0a  30163  cdlemg31a  30165  cdlemg31b  30166  ltrnco  30187  cdlemg48  30205  tgrpov  30216  tendoco2  30236  tendoplco2  30247  cdlemh1  30283  cdlemk1  30299  cdlemk26b-3  30373  cdlemk27-3  30375  cdlemk28-3  30376  cdlemk34  30378  cdlemkfid1N  30389  cdlemkid3N  30401  cdlemkid4  30402  cdlemk35s-id  30406  cdlemk39s-id  30408  cdlemk51  30421  tendospcanN  30492  cdlemm10N  30587  dicvaddcl  30659  dicvscacl  30660  cdlemn6  30671  dihvalcq2  30716  dihord6b  30729  dihord5apre  30731  dihglbcpreN  30769  dihjatc1  30780  dihmeetlem20N  30795  dih1dimatlem0  30797  dihglblem6  30809  dochexmidlem4  30932  mapdpglem32  31174  mapdh8ad  31248  mapdh9aOLDN  31260  hdmap11lem2  31314  hdmap14lem6  31345
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