MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3r 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  4171  tfisi  4797  f1oiso2  6031  omeulem1  6784  omeulem2  6785  elfiun  7393  isfin2-2  8155  addid2  9205  mulcan  9615  mulcan2  9616  divass  9652  divdir  9657  div11  9660  ltdiv1  9830  ltmuldiv  9836  lediv2  9856  xaddass2  10785  xlt2add  10795  expaddz  11379  expmulz  11381  resqrex  12011  resqrcl  12014  o1add  12362  o1mul  12363  o1sub  12364  dvdsgcd  12998  rpexp12i  13077  pythagtriplem4  13148  pythagtriplem11  13154  pythagtriplem13  13156  pcpremul  13172  pceu  13175  pcqmul  13182  pcqdiv  13186  f1ocpbllem  13704  funcoppc  14027  funcres  14048  catcisolem  14216  1stfcl  14249  2ndfcl  14250  prfcl  14255  evlfcl  14274  curf1cl  14280  curfcl  14284  hofcl  14311  latjlej12  14451  latmlem12  14467  latj4  14485  latj4rot  14486  odcong  15142  cmn4  15386  ablsub4  15392  abladdsub4  15393  lsm4  15430  abvdom  15881  abvtrivd  15883  lspsolvlem  16169  lbsextlem2  16186  hausflimlem  17964  psmetlecl  18299  xmetlecl  18329  prdsxmetlem  18351  xblcntrps  18393  xblcntr  18394  bndth  18936  cph2ass  19128  iscau3  19184  dvres2  19752  coemullem  20121  vieta1  20182  aalioulem4  20205  cxpcn3lem  20584  angcan  20597  divsqrsumlem  20771  dchrmusumlema  21140  dchrvmasumlema  21147  dchrisum0lema  21161  logdivsum  21180  padicabv  21277  gxnval  21801  gxnn0mul  21818  adjlnop  23542  xreceu  24121  ofldmul  24192  rhmdvd  24212  measvunilem  24519  measvuni  24521  ax5seglem3  25774  ax5seglem6  25777  axpasch  25784  axeuclid  25806  axcontlem4  25810  axcontlem8  25814  cgrcomim  25827  cgrcoml  25834  cgrcomr  25835  cgrdegen  25842  segconeu  25849  btwnintr  25857  btwnexch3  25858  btwnouttr2  25860  btwnouttr  25862  btwnexch  25863  ifscgr  25882  lineext  25914  linecgr  25919  lineid  25921  idinside  25922  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem14  25938  btwnconn2  25940  btwnconn3  25941  midofsegid  25942  btwnoutside  25963  outsideoftr  25967  lineunray  25985  lineelsb2  25986  itg2addnclem  26155  cnres2  26362  heibor  26420  mzpmfp  26694  mzpsubst  26695  pellex  26788  pellfundex  26839  pellfund14gap  26840  qirropth  26861  rmxypos  26902  congmul  26922  congsub  26925  mzpcong  26927  coprmdvdsb  26942  jm2.15nn0  26964  jm2.16nn0  26965  rpnnen3lem  26992  symgsssg  27276  symgfisg  27277  idomsubgmo  27382  bnj1128  29065  lsmcv2  29512  lcvat  29513  lcvexchlem4  29520  lcvexchlem5  29521  lfladd  29549  lflsub  29550  lflmul  29551  lshpkrlem4  29596  latm4  29716  omlmod1i2N  29743  cvlsupr7  29831  cvlsupr8  29832  hlatj4  29856  hlrelat3  29894  cvrval3  29895  atcvrj1  29913  atlelt  29920  2atlt  29921  2atjm  29927  3noncolr2  29931  athgt  29938  3dimlem2  29941  3dimlem4OLDN  29947  1cvratex  29955  ps-1  29959  ps-2  29960  hlatexch3N  29962  llnle  30000  atcvrlln2  30001  atcvrlln  30002  lplni2  30019  lplnle  30022  lplnnle2at  30023  lplnnlelln  30025  llncvrlpln2  30039  2llnmeqat  30053  lvolnle3at  30064  lvolnlelln  30066  4atlem0ae  30076  lneq2at  30260  lnjatN  30262  lncvrat  30264  2lnat  30266  elpaddri  30284  paddasslem2  30303  padd4N  30322  hlmod1i  30338  llnexchb2  30351  dalawlem2  30354  pclfinN  30382  pexmidlem4N  30455  pl42lem1N  30461  lhp2lt  30483  lhpexle1  30490  lhpexle2lem  30491  lhpj1  30504  lhpmcvr5N  30509  lhp2at0  30514  lhp2at0nle  30517  lhple  30524  lhpat  30525  lhpat4N  30526  4atexlemnslpq  30538  4atexlem7  30557  ltrn11  30608  ltrnle  30611  ltrnm  30613  ltrnj  30614  ltrncvr  30615  ltrnel  30621  ltrncnvel  30624  ltrncnv  30628  ltrnmw  30633  trlat  30651  trl0  30652  trlnidat  30655  trlnid  30661  ltrnatlw  30665  trlne  30667  trlval4  30670  cdlemc5  30677  cdlemd2  30681  cdlemd7  30686  cdlemd8  30687  cdlemd9  30688  cdleme0c  30695  cdleme0e  30699  cdleme0fN  30700  cdleme3g  30716  cdleme3h  30717  cdleme5  30722  cdleme11c  30743  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme0nex  30772  cdleme18a  30773  cdleme22gb  30776  cdleme20zN  30783  cdleme20y  30784  cdleme20c  30793  cdleme20k  30801  cdleme21a  30807  cdleme21b  30808  cdleme21c  30809  cdleme21ct  30811  cdleme21h  30816  cdleme22d  30825  cdleme22f  30828  cdleme26ee  30842  cdleme30a  30860  cdlemefs45eN  30913  cdleme36a  30942  cdleme36m  30943  cdleme39a  30947  cdleme42b  30960  cdleme43dN  30974  cdlemeg47rv2  30992  cdlemeg46sfg  31002  cdlemeg46rjgN  31004  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdleme48d  31017  cdleme50ltrn  31039  cdlemf1  31043  cdlemf  31045  cdlemg2dN  31072  cdlemg2fvlem  31076  cdlemg2l  31085  cdlemg7fvbwN  31089  cdlemg7aN  31107  cdlemg10c  31121  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg18a  31160  cdlemg18b  31161  cdlemg31b0a  31177  cdlemg31a  31179  cdlemg31b  31180  ltrnco  31201  cdlemg48  31219  tgrpov  31230  tendoco2  31250  tendoplco2  31261  cdlemh1  31297  cdlemk1  31313  cdlemk26b-3  31387  cdlemk27-3  31389  cdlemk28-3  31390  cdlemk34  31392  cdlemkfid1N  31403  cdlemkid3N  31415  cdlemkid4  31416  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk51  31435  tendospcanN  31506  cdlemm10N  31601  dicvaddcl  31673  dicvscacl  31674  cdlemn6  31685  dihvalcq2  31730  dihord6b  31743  dihord5apre  31745  dihglbcpreN  31783  dihjatc1  31794  dihmeetlem20N  31809  dih1dimatlem0  31811  dihglblem6  31823  dochexmidlem4  31946  mapdpglem32  32188  mapdh8ad  32262  mapdh9aOLDN  32274  hdmap11lem2  32328  hdmap14lem6  32359
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