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

Theorem simp3r 986
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 448 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl3r  1013  simpr3r  1019  simp13r  1073  simp23r  1079  simp33r  1085  disjss3  4203  tfisi  4830  f1oiso2  6064  omeulem1  6817  omeulem2  6818  elfiun  7427  isfin2-2  8191  addid2  9241  mulcan  9651  mulcan2  9652  divass  9688  divdir  9693  div11  9696  ltdiv1  9866  ltmuldiv  9872  lediv2  9892  xaddass2  10821  xlt2add  10831  expaddz  11416  expmulz  11418  resqrex  12048  resqrcl  12051  o1add  12399  o1mul  12400  o1sub  12401  dvdsgcd  13035  rpexp12i  13114  pythagtriplem4  13185  pythagtriplem11  13191  pythagtriplem13  13193  pcpremul  13209  pceu  13212  pcqmul  13219  pcqdiv  13223  f1ocpbllem  13741  funcoppc  14064  funcres  14085  catcisolem  14253  1stfcl  14286  2ndfcl  14287  prfcl  14292  evlfcl  14311  curf1cl  14317  curfcl  14321  hofcl  14348  latjlej12  14488  latmlem12  14504  latj4  14522  latj4rot  14523  odcong  15179  cmn4  15423  ablsub4  15429  abladdsub4  15430  lsm4  15467  abvdom  15918  abvtrivd  15920  lspsolvlem  16206  lbsextlem2  16223  hausflimlem  18003  psmetlecl  18338  xmetlecl  18368  prdsxmetlem  18390  xblcntrps  18432  xblcntr  18433  bndth  18975  cph2ass  19167  iscau3  19223  dvres2  19791  coemullem  20160  vieta1  20221  aalioulem4  20244  cxpcn3lem  20623  angcan  20636  divsqrsumlem  20810  dchrmusumlema  21179  dchrvmasumlema  21186  dchrisum0lema  21200  logdivsum  21219  padicabv  21316  gxnval  21840  gxnn0mul  21857  adjlnop  23581  xreceu  24160  ofldmul  24231  rhmdvd  24251  measvunilem  24558  measvuni  24560  ax5seglem3  25862  ax5seglem6  25865  axpasch  25872  axeuclid  25894  axcontlem4  25898  axcontlem8  25902  cgrcomim  25915  cgrcoml  25922  cgrcomr  25923  cgrdegen  25930  segconeu  25937  btwnintr  25945  btwnexch3  25946  btwnouttr2  25948  btwnouttr  25950  btwnexch  25951  ifscgr  25970  lineext  26002  linecgr  26007  lineid  26009  idinside  26010  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem14  26026  btwnconn2  26028  btwnconn3  26029  midofsegid  26030  btwnoutside  26051  outsideoftr  26055  lineunray  26073  lineelsb2  26074  itg2addnclem  26246  cnres2  26463  heibor  26521  mzpmfp  26795  mzpsubst  26796  pellex  26889  pellfundex  26940  pellfund14gap  26941  qirropth  26962  rmxypos  27003  congmul  27023  congsub  27026  mzpcong  27028  coprmdvdsb  27043  jm2.15nn0  27065  jm2.16nn0  27066  rpnnen3lem  27093  symgsssg  27376  symgfisg  27377  idomsubgmo  27482  bnj1128  29296  lsmcv2  29764  lcvat  29765  lcvexchlem4  29772  lcvexchlem5  29773  lfladd  29801  lflsub  29802  lflmul  29803  lshpkrlem4  29848  latm4  29968  omlmod1i2N  29995  cvlsupr7  30083  cvlsupr8  30084  hlatj4  30108  hlrelat3  30146  cvrval3  30147  atcvrj1  30165  atlelt  30172  2atlt  30173  2atjm  30179  3noncolr2  30183  athgt  30190  3dimlem2  30193  3dimlem4OLDN  30199  1cvratex  30207  ps-1  30211  ps-2  30212  hlatexch3N  30214  llnle  30252  atcvrlln2  30253  atcvrlln  30254  lplni2  30271  lplnle  30274  lplnnle2at  30275  lplnnlelln  30277  llncvrlpln2  30291  2llnmeqat  30305  lvolnle3at  30316  lvolnlelln  30318  4atlem0ae  30328  lneq2at  30512  lnjatN  30514  lncvrat  30516  2lnat  30518  elpaddri  30536  paddasslem2  30555  padd4N  30574  hlmod1i  30590  llnexchb2  30603  dalawlem2  30606  pclfinN  30634  pexmidlem4N  30707  pl42lem1N  30713  lhp2lt  30735  lhpexle1  30742  lhpexle2lem  30743  lhpj1  30756  lhpmcvr5N  30761  lhp2at0  30766  lhp2at0nle  30769  lhple  30776  lhpat  30777  lhpat4N  30778  4atexlemnslpq  30790  4atexlem7  30809  ltrn11  30860  ltrnle  30863  ltrnm  30865  ltrnj  30866  ltrncvr  30867  ltrnel  30873  ltrncnvel  30876  ltrncnv  30880  ltrnmw  30885  trlat  30903  trl0  30904  trlnidat  30907  trlnid  30913  ltrnatlw  30917  trlne  30919  trlval4  30922  cdlemc5  30929  cdlemd2  30933  cdlemd7  30938  cdlemd8  30939  cdlemd9  30940  cdleme0c  30947  cdleme0e  30951  cdleme0fN  30952  cdleme3g  30968  cdleme3h  30969  cdleme5  30974  cdleme11c  30995  cdleme11h  31000  cdleme11j  31001  cdleme11k  31002  cdleme0nex  31024  cdleme18a  31025  cdleme22gb  31028  cdleme20zN  31035  cdleme20y  31036  cdleme20c  31045  cdleme20k  31053  cdleme21a  31059  cdleme21b  31060  cdleme21c  31061  cdleme21ct  31063  cdleme21h  31068  cdleme22d  31077  cdleme22f  31080  cdleme26ee  31094  cdleme30a  31112  cdlemefs45eN  31165  cdleme36a  31194  cdleme36m  31195  cdleme39a  31199  cdleme42b  31212  cdleme43dN  31226  cdlemeg47rv2  31244  cdlemeg46sfg  31254  cdlemeg46rjgN  31256  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemeg46gfv  31264  cdleme48d  31269  cdleme50ltrn  31291  cdlemf1  31295  cdlemf  31297  cdlemg2dN  31324  cdlemg2fvlem  31328  cdlemg2l  31337  cdlemg7fvbwN  31341  cdlemg7aN  31359  cdlemg10c  31373  cdlemg17a  31395  cdlemg17dALTN  31398  cdlemg18a  31412  cdlemg18b  31413  cdlemg31b0a  31429  cdlemg31a  31431  cdlemg31b  31432  ltrnco  31453  cdlemg48  31471  tgrpov  31482  tendoco2  31502  tendoplco2  31513  cdlemh1  31549  cdlemk1  31565  cdlemk26b-3  31639  cdlemk27-3  31641  cdlemk28-3  31642  cdlemk34  31644  cdlemkfid1N  31655  cdlemkid3N  31667  cdlemkid4  31668  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk51  31687  tendospcanN  31758  cdlemm10N  31853  dicvaddcl  31925  dicvscacl  31926  cdlemn6  31937  dihvalcq2  31982  dihord6b  31995  dihord5apre  31997  dihglbcpreN  32035  dihjatc1  32046  dihmeetlem20N  32061  dih1dimatlem0  32063  dihglblem6  32075  dochexmidlem4  32198  mapdpglem32  32440  mapdh8ad  32514  mapdh9aOLDN  32526  hdmap11lem2  32580  hdmap14lem6  32611
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