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  4152  tfisi  4778  omeulem1  6761  omeulem2  6762  uniinqs  6920  elfiun  7370  tcrank  7741  isfin2-2  8132  konigthlem  8376  gruen  8620  addid2  9181  mulcan  9591  mulcan2  9592  divass  9628  divdir  9633  div11  9636  divcan5  9648  ltmul1  9792  ltdiv1  9806  ltmuldiv  9812  lediv2  9832  xaddass2  10761  xlt2add  10771  xmulasslem3  10797  xadddi2  10808  expaddz  11351  expmulz  11353  resqrcl  11986  o1add  12334  o1mul  12335  o1sub  12336  dvdsadd2b  12819  dvdsgcd  12970  rpexp12i  13049  pythagtriplem3  13119  pcpremul  13144  pceu  13147  pcqmul  13154  pcqdiv  13158  f1ocpbllem  13676  funcoppc  13999  funcres  14020  catcisolem  14188  1stfcl  14221  2ndfcl  14222  prfcl  14227  evlfcl  14246  curf1cl  14252  curfcl  14256  hofcl  14283  latjlej12  14423  latmlem12  14439  latj4  14457  latj4rot  14458  odcong  15114  cmn4  15358  ablsub4  15364  abladdsub4  15365  lsm4  15402  abvdom  15853  abvres  15854  abvtrivd  15855  lspsolvlem  16141  lbsextlem2  16158  nllyrest  17470  hausflimlem  17932  tsmsxp  18105  xmetlecl  18285  prdsxmetlem  18306  bndth  18854  cph2ass  19046  iscau3  19102  dvres2  19666  coemullem  20035  vieta1  20096  aalioulem4  20119  cxpcn3lem  20498  angcan  20511  dchrvmasumlema  21061  logdivsum  21094  abvcxp  21176  padicabv  21191  gxneg  21702  gxsuc  21708  gxmodid  21715  adjlnop  23437  xreceu  24006  rhmdvd  24075  measvunilem  24360  measvunilem0  24361  measres  24370  subdivcomb1  24974  subdivcomb2  24975  ax5seglem3  25584  ax5seglem6  25587  axpasch  25594  axeuclid  25616  axcontlem4  25620  axcontlem8  25624  cgrcomim  25637  cgrcoml  25644  cgrcomr  25645  cgrdegen  25652  segconeu  25659  btwnintr  25667  btwnexch3  25668  btwnouttr2  25670  btwnouttr  25672  btwnexch  25673  trisegint  25676  lineext  25724  linecgr  25729  lineid  25731  idinside  25732  btwnconn1lem3  25737  btwnconn1lem4  25738  btwnconn1lem7  25741  btwnconn1lem14  25748  btwnconn2  25750  midofsegid  25752  btwnoutside  25773  outsideoftr  25777  lineunray  25795  lineelsb2  25796  cnres2  26163  heibor  26221  mzpsubst  26496  pellex  26589  pellfundex  26640  pellfund14gap  26641  qirropth  26662  rmxypos  26703  congmul  26723  congsub  26726  mzpcong  26728  coprmdvdsb  26743  jm2.15nn0  26765  jm2.16nn0  26766  rpnnen3lem  26793  symgsssg  27077  symgfisg  27078  psgnunilem4  27089  idomsubgmo  27183  stoweidlem57  27474  bnj1128  28697  lsmcv2  29144  lcvat  29145  lcvexchlem4  29152  lcvexchlem5  29153  lfladd  29181  lflsub  29182  lflmul  29183  lshpkrlem4  29228  latm4  29348  omlmod1i2N  29375  cvlatexch3  29453  cvlsupr7  29463  hlatj4  29488  hlrelat3  29526  cvrval3  29527  atcvrj1  29545  atlelt  29552  2atlt  29553  2atjm  29559  3noncolr2  29563  athgt  29570  3dimlem2  29573  3dimlem4  29578  3dimlem4OLDN  29579  3dim3  29583  1cvratex  29587  ps-1  29591  ps-2  29592  hlatexch3N  29594  llnle  29632  atcvrlln2  29633  atcvrlln  29634  lplni2  29651  lplnle  29654  lplnnle2at  29655  llncvrlpln2  29671  lplnexllnN  29678  2llnmeqat  29685  lvolnle3at  29696  4atlem0ae  29708  lplncvrlvol2  29729  lnjatN  29894  lncvrat  29896  cdlemblem  29907  elpaddri  29916  paddasslem2  29935  paddasslem16  29949  padd4N  29954  hlmod1i  29970  dalawlem2  29986  pclfinN  30014  pexmidlem4N  30087  pl42lem1N  30093  lhp2lt  30115  lhpexle1  30122  lhpexle2lem  30123  lhpj1  30136  lhpmcvr5N  30141  lhp2at0  30146  lhp2atnle  30147  lhp2at0nle  30149  lhple  30156  lhpat  30157  lhpat4N  30158  4atexlempnq  30169  4atexlem7  30189  4atex  30190  ltrn11  30240  ltrnle  30243  ltrnm  30245  ltrnj  30246  ltrncvr  30247  ltrnel  30253  ltrncnvel  30256  ltrncnv  30260  ltrnmw  30265  trlval2  30277  trlcnv  30279  trljat1  30280  trljat2  30281  trlat  30283  trl0  30284  trlnidat  30287  trlnid  30293  cdlemc1  30305  cdlemc2  30306  cdlemc5  30309  cdlemd2  30313  cdlemd7  30318  cdlemd8  30319  cdlemd9  30320  cdleme0e  30331  cdleme3g  30348  cdleme3h  30349  cdleme3  30351  cdleme5  30354  cdleme10  30368  cdleme11a  30374  cdleme11c  30375  cdleme11h  30380  cdleme11j  30381  cdleme0nex  30404  cdleme18a  30405  cdleme18b  30406  cdleme22gb  30408  cdleme20zN  30415  cdleme20y  30416  cdleme20c  30425  cdleme20k  30433  cdleme21a  30439  cdleme21b  30440  cdleme21c  30441  cdleme21h  30448  cdleme22b  30455  cdleme22d  30457  cdleme22f  30460  cdleme25a  30467  cdleme25c  30469  cdleme25dN  30470  cdleme26ee  30474  cdleme30a  30492  cdlemefr29bpre0N  30520  cdlemefr29clN  30521  cdlemefr32fvaN  30523  cdlemefr32fva1  30524  cdlemefs29bpre0N  30530  cdlemefs29bpre1N  30531  cdlemefs29cpre1N  30532  cdlemefs29clN  30533  cdleme43fsv1snlem  30534  cdlemefs32fvaN  30536  cdlemefs32fva1  30537  cdlemefs31fv1  30538  cdleme36a  30574  cdleme39a  30579  cdleme42a  30585  cdleme42c  30586  cdleme17d3  30610  cdleme48fv  30613  cdleme48bw  30616  cdleme48b  30617  cdlemeg46rgv  30642  cdlemeg46req  30643  cdlemeg46gfv  30644  cdleme48d  30649  cdleme50trn2a  30664  cdleme50trn2  30665  cdleme50ltrn  30671  cdlemf1  30675  cdlemf  30677  trlord  30683  cdlemg2dN  30704  cdlemg2fvlem  30708  cdlemg2l  30717  cdlemg7fvbwN  30721  cdlemg7aN  30739  cdlemg10bALTN  30750  cdlemg10c  30753  cdlemg17a  30775  cdlemg17dALTN  30778  cdlemg31b0a  30809  cdlemg31a  30811  cdlemg31b  30812  cdlemg34  30826  cdlemg36  30828  ltrnco  30833  trlcoabs2N  30836  trlcolem  30840  cdlemg48  30851  tgrpov  30862  tendoco2  30882  tendoplco2  30893  cdlemh1  30929  cdlemi1  30932  cdlemi2  30933  cdlemj3  30937  tendoid0  30939  cdlemk1  30945  cdlemk2  30946  cdlemk4  30948  cdlemk8  30952  cdlemk9  30953  cdlemk9bN  30954  cdlemk10  30957  cdlemk26b-3  31019  cdlemk26-3  31020  cdlemk28-3  31022  cdlemk37  31028  cdlemk39  31030  cdlemkfid1N  31035  cdlemkid1  31036  cdlemky  31040  cdlemkyu  31041  cdlemk19ylem  31044  cdlemk19xlem  31056  cdlemk11t  31060  cdlemk51  31067  cdlemkyyN  31076  cdleml6  31095  cdleml7  31096  cdleml8  31097  cdleml9  31098  erngdvlem4  31105  erngdvlem4-rN  31113  tendospcanN  31138  dia11N  31163  cdlemm10N  31233  dib11N  31275  dicvaddcl  31305  dicvscacl  31306  cdlemn6  31317  dihvalcq2  31362  dihopelvalcpre  31363  dihord6b  31375  dihord5apre  31377  dihmeetlem1N  31405  dihmeetlem2N  31414  dihglbcpreN  31415  dihjatc1  31426  dihmeetlem20N  31441  dih1dimatlem0  31443  dihatlat  31449  dihglblem6  31455  dochexmidlem4  31578  mapdpglem32  31820  mapdh8ad  31894  mapdh9aOLDN  31906  hdmap11lem2  31960  hdmap14lem6  31991
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