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  4022  tfisi  4649  f1oiso2  5849  omeulem1  6580  omeulem2  6581  elfiun  7183  isfin2-2  7945  addid2  8995  mulcan  9405  mulcan2  9406  divass  9442  divdir  9447  div11  9450  ltdiv1  9620  ltmuldiv  9626  lediv2  9646  xaddass2  10570  xlt2add  10580  expaddz  11146  expmulz  11148  resqrex  11736  resqrcl  11739  o1add  12087  o1mul  12088  o1sub  12089  dvdsgcd  12722  rpexp12i  12801  pythagtriplem4  12872  pythagtriplem11  12878  pythagtriplem13  12880  pcpremul  12896  pceu  12899  pcqmul  12906  pcqdiv  12910  f1ocpbllem  13426  funcoppc  13749  funcres  13770  catcisolem  13938  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  latjlej12  14173  latmlem12  14189  latj4  14207  latj4rot  14208  odcong  14864  cmn4  15108  ablsub4  15114  abladdsub4  15115  lsm4  15152  abvdom  15603  abvtrivd  15605  lspsolvlem  15895  lbsextlem2  15912  hausflimlem  17674  xmetlecl  17911  prdsxmetlem  17932  xblcntr  17963  bndth  18456  cph2ass  18648  iscau3  18704  dvres2  19262  coemullem  19631  vieta1  19692  aalioulem4  19715  cxpcn3lem  20087  angcan  20100  divsqrsumlem  20274  dchrmusumlema  20642  dchrvmasumlema  20649  dchrisum0lema  20663  logdivsum  20682  padicabv  20779  gxnval  20927  gxnn0mul  20944  adjlnop  22666  xreceu  23105  measvunilem  23540  measvuni  23542  ax5seglem3  24559  ax5seglem6  24562  axpasch  24569  axeuclid  24591  axcontlem4  24595  axcontlem8  24599  cgrcomim  24612  cgrcoml  24619  cgrcomr  24620  cgrdegen  24627  segconeu  24634  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  btwnouttr  24647  btwnexch  24648  ifscgr  24667  lineext  24699  linecgr  24704  lineid  24706  idinside  24707  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem14  24723  btwnconn2  24725  btwnconn3  24726  midofsegid  24727  btwnoutside  24748  outsideoftr  24752  lineunray  24770  lineelsb2  24771  infxpg  25095  valvalcurfn  25206  prltub  25260  mulinvsca  25480  conttnf2  25562  prdnei  25573  mulmulvec  25687  distsava  25689  cmpmorass  25966  lppotos  26144  cnres2  26483  heibor  26545  mzpmfp  26825  mzpsubst  26826  pellex  26920  pellfundex  26971  pellfund14gap  26972  qirropth  26993  rmxypos  27034  congmul  27054  congsub  27057  mzpcong  27059  coprmdvdsb  27074  jm2.15nn0  27096  jm2.16nn0  27097  rpnnen3lem  27124  symgsssg  27408  symgfisg  27409  idomsubgmo  27514  bnj1128  29020  lsmcv2  29219  lcvat  29220  lcvexchlem4  29227  lcvexchlem5  29228  lfladd  29256  lflsub  29257  lflmul  29258  lshpkrlem4  29303  latm4  29423  omlmod1i2N  29450  cvlsupr7  29538  cvlsupr8  29539  hlatj4  29563  hlrelat3  29601  cvrval3  29602  atcvrj1  29620  atlelt  29627  2atlt  29628  2atjm  29634  3noncolr2  29638  athgt  29645  3dimlem2  29648  3dimlem4OLDN  29654  1cvratex  29662  ps-1  29666  ps-2  29667  hlatexch3N  29669  llnle  29707  atcvrlln2  29708  atcvrlln  29709  lplni2  29726  lplnle  29729  lplnnle2at  29730  lplnnlelln  29732  llncvrlpln2  29746  2llnmeqat  29760  lvolnle3at  29771  lvolnlelln  29773  4atlem0ae  29783  lneq2at  29967  lnjatN  29969  lncvrat  29971  2lnat  29973  elpaddri  29991  paddasslem2  30010  padd4N  30029  hlmod1i  30045  llnexchb2  30058  dalawlem2  30061  pclfinN  30089  pexmidlem4N  30162  pl42lem1N  30168  lhp2lt  30190  lhpexle1  30197  lhpexle2lem  30198  lhpj1  30211  lhpmcvr5N  30216  lhp2at0  30221  lhp2at0nle  30224  lhple  30231  lhpat  30232  lhpat4N  30233  4atexlemnslpq  30245  4atexlem7  30264  ltrn11  30315  ltrnle  30318  ltrnm  30320  ltrnj  30321  ltrncvr  30322  ltrnel  30328  ltrncnvel  30331  ltrncnv  30335  ltrnmw  30340  trlat  30358  trl0  30359  trlnidat  30362  trlnid  30368  ltrnatlw  30372  trlne  30374  trlval4  30377  cdlemc5  30384  cdlemd2  30388  cdlemd7  30393  cdlemd8  30394  cdlemd9  30395  cdleme0c  30402  cdleme0e  30406  cdleme0fN  30407  cdleme3g  30423  cdleme3h  30424  cdleme5  30429  cdleme11c  30450  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme0nex  30479  cdleme18a  30480  cdleme22gb  30483  cdleme20zN  30490  cdleme20y  30491  cdleme20c  30500  cdleme20k  30508  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme21ct  30518  cdleme21h  30523  cdleme22d  30532  cdleme22f  30535  cdleme26ee  30549  cdleme30a  30567  cdlemefs45eN  30620  cdleme36a  30649  cdleme36m  30650  cdleme39a  30654  cdleme42b  30667  cdleme43dN  30681  cdlemeg47rv2  30699  cdlemeg46sfg  30709  cdlemeg46rjgN  30711  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdleme48d  30724  cdleme50ltrn  30746  cdlemf1  30750  cdlemf  30752  cdlemg2dN  30779  cdlemg2fvlem  30783  cdlemg2l  30792  cdlemg7fvbwN  30796  cdlemg7aN  30814  cdlemg10c  30828  cdlemg17a  30850  cdlemg17dALTN  30853  cdlemg18a  30867  cdlemg18b  30868  cdlemg31b0a  30884  cdlemg31a  30886  cdlemg31b  30887  ltrnco  30908  cdlemg48  30926  tgrpov  30937  tendoco2  30957  tendoplco2  30968  cdlemh1  31004  cdlemk1  31020  cdlemk26b-3  31094  cdlemk27-3  31096  cdlemk28-3  31097  cdlemk34  31099  cdlemkfid1N  31110  cdlemkid3N  31122  cdlemkid4  31123  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk51  31142  tendospcanN  31213  cdlemm10N  31308  dicvaddcl  31380  dicvscacl  31381  cdlemn6  31392  dihvalcq2  31437  dihord6b  31450  dihord5apre  31452  dihglbcpreN  31490  dihjatc1  31501  dihmeetlem20N  31516  dih1dimatlem0  31518  dihglblem6  31530  dochexmidlem4  31653  mapdpglem32  31895  mapdh8ad  31969  mapdh9aOLDN  31981  hdmap11lem2  32035  hdmap14lem6  32066
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