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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl3l  1012  simpr3l  1018  simp13l  1072  simp23l  1078  simp33l  1084  disjss3  4171  tfisi  4797  omeulem1  6784  omeulem2  6785  uniinqs  6943  elfiun  7393  tcrank  7764  isfin2-2  8155  konigthlem  8399  gruen  8643  addid2  9205  mulcan  9615  mulcan2  9616  divass  9652  divdir  9657  div11  9660  divcan5  9672  ltmul1  9816  ltdiv1  9830  ltmuldiv  9836  lediv2  9856  xaddass2  10785  xlt2add  10795  xmulasslem3  10821  xadddi2  10832  expaddz  11379  expmulz  11381  resqrcl  12014  o1add  12362  o1mul  12363  o1sub  12364  dvdsadd2b  12847  dvdsgcd  12998  rpexp12i  13077  pythagtriplem3  13147  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  abvres  15882  abvtrivd  15883  lspsolvlem  16169  lbsextlem2  16186  nllyrest  17502  hausflimlem  17964  tsmsxp  18137  psmetlecl  18299  xmetlecl  18329  prdsxmetlem  18351  bndth  18936  cph2ass  19128  iscau3  19184  dvres2  19752  coemullem  20121  vieta1  20182  aalioulem4  20205  cxpcn3lem  20584  angcan  20597  dchrvmasumlema  21147  logdivsum  21180  abvcxp  21262  padicabv  21277  gxneg  21807  gxsuc  21813  gxmodid  21820  adjlnop  23542  xreceu  24121  rhmdvd  24212  measvunilem  24519  measvunilem0  24520  measres  24529  subdivcomb1  25148  subdivcomb2  25149  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  trisegint  25866  lineext  25914  linecgr  25919  lineid  25921  idinside  25922  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem7  25931  btwnconn1lem14  25938  btwnconn2  25940  midofsegid  25942  btwnoutside  25963  outsideoftr  25967  lineunray  25985  lineelsb2  25986  cnres2  26362  heibor  26420  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  psgnunilem4  27288  idomsubgmo  27382  stoweidlem57  27673  bnj1128  29065  lsmcv2  29512  lcvat  29513  lcvexchlem4  29520  lcvexchlem5  29521  lfladd  29549  lflsub  29550  lflmul  29551  lshpkrlem4  29596  latm4  29716  omlmod1i2N  29743  cvlatexch3  29821  cvlsupr7  29831  hlatj4  29856  hlrelat3  29894  cvrval3  29895  atcvrj1  29913  atlelt  29920  2atlt  29921  2atjm  29927  3noncolr2  29931  athgt  29938  3dimlem2  29941  3dimlem4  29946  3dimlem4OLDN  29947  3dim3  29951  1cvratex  29955  ps-1  29959  ps-2  29960  hlatexch3N  29962  llnle  30000  atcvrlln2  30001  atcvrlln  30002  lplni2  30019  lplnle  30022  lplnnle2at  30023  llncvrlpln2  30039  lplnexllnN  30046  2llnmeqat  30053  lvolnle3at  30064  4atlem0ae  30076  lplncvrlvol2  30097  lnjatN  30262  lncvrat  30264  cdlemblem  30275  elpaddri  30284  paddasslem2  30303  paddasslem16  30317  padd4N  30322  hlmod1i  30338  dalawlem2  30354  pclfinN  30382  pexmidlem4N  30455  pl42lem1N  30461  lhp2lt  30483  lhpexle1  30490  lhpexle2lem  30491  lhpj1  30504  lhpmcvr5N  30509  lhp2at0  30514  lhp2atnle  30515  lhp2at0nle  30517  lhple  30524  lhpat  30525  lhpat4N  30526  4atexlempnq  30537  4atexlem7  30557  4atex  30558  ltrn11  30608  ltrnle  30611  ltrnm  30613  ltrnj  30614  ltrncvr  30615  ltrnel  30621  ltrncnvel  30624  ltrncnv  30628  ltrnmw  30633  trlval2  30645  trlcnv  30647  trljat1  30648  trljat2  30649  trlat  30651  trl0  30652  trlnidat  30655  trlnid  30661  cdlemc1  30673  cdlemc2  30674  cdlemc5  30677  cdlemd2  30681  cdlemd7  30686  cdlemd8  30687  cdlemd9  30688  cdleme0e  30699  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme5  30722  cdleme10  30736  cdleme11a  30742  cdleme11c  30743  cdleme11h  30748  cdleme11j  30749  cdleme0nex  30772  cdleme18a  30773  cdleme18b  30774  cdleme22gb  30776  cdleme20zN  30783  cdleme20y  30784  cdleme20c  30793  cdleme20k  30801  cdleme21a  30807  cdleme21b  30808  cdleme21c  30809  cdleme21h  30816  cdleme22b  30823  cdleme22d  30825  cdleme22f  30828  cdleme25a  30835  cdleme25c  30837  cdleme25dN  30838  cdleme26ee  30842  cdleme30a  30860  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdleme43fsv1snlem  30902  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdlemefs31fv1  30906  cdleme36a  30942  cdleme39a  30947  cdleme42a  30953  cdleme42c  30954  cdleme17d3  30978  cdleme48fv  30981  cdleme48bw  30984  cdleme48b  30985  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdleme48d  31017  cdleme50trn2a  31032  cdleme50trn2  31033  cdleme50ltrn  31039  cdlemf1  31043  cdlemf  31045  trlord  31051  cdlemg2dN  31072  cdlemg2fvlem  31076  cdlemg2l  31085  cdlemg7fvbwN  31089  cdlemg7aN  31107  cdlemg10bALTN  31118  cdlemg10c  31121  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg31b0a  31177  cdlemg31a  31179  cdlemg31b  31180  cdlemg34  31194  cdlemg36  31196  ltrnco  31201  trlcoabs2N  31204  trlcolem  31208  cdlemg48  31219  tgrpov  31230  tendoco2  31250  tendoplco2  31261  cdlemh1  31297  cdlemi1  31300  cdlemi2  31301  cdlemj3  31305  tendoid0  31307  cdlemk1  31313  cdlemk2  31314  cdlemk4  31316  cdlemk8  31320  cdlemk9  31321  cdlemk9bN  31322  cdlemk10  31325  cdlemk26b-3  31387  cdlemk26-3  31388  cdlemk28-3  31390  cdlemk37  31396  cdlemk39  31398  cdlemkfid1N  31403  cdlemkid1  31404  cdlemky  31408  cdlemkyu  31409  cdlemk19ylem  31412  cdlemk19xlem  31424  cdlemk11t  31428  cdlemk51  31435  cdlemkyyN  31444  cdleml6  31463  cdleml7  31464  cdleml8  31465  cdleml9  31466  erngdvlem4  31473  erngdvlem4-rN  31481  tendospcanN  31506  dia11N  31531  cdlemm10N  31601  dib11N  31643  dicvaddcl  31673  dicvscacl  31674  cdlemn6  31685  dihvalcq2  31730  dihopelvalcpre  31731  dihord6b  31743  dihord5apre  31745  dihmeetlem1N  31773  dihmeetlem2N  31782  dihglbcpreN  31783  dihjatc1  31794  dihmeetlem20N  31809  dih1dimatlem0  31811  dihatlat  31817  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