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

Theorem simp3l 983
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 443 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl3l  1010  simpr3l  1016  simp13l  1070  simp23l  1076  simp33l  1082  disjss3  4038  tfisi  4665  omeulem1  6596  omeulem2  6597  elfiun  7199  tcrank  7570  isfin2-2  7961  konigthlem  8206  gruen  8450  addid2  9011  mulcan  9421  mulcan2  9422  divass  9458  divdir  9463  div11  9466  divcan5  9478  ltmul1  9622  ltdiv1  9636  ltmuldiv  9642  lediv2  9662  xaddass2  10586  xlt2add  10596  xmulasslem3  10622  xadddi2  10633  expaddz  11162  expmulz  11164  resqrcl  11755  o1add  12103  o1mul  12104  o1sub  12105  dvdsadd2b  12587  dvdsgcd  12738  rpexp12i  12817  pythagtriplem3  12887  pcpremul  12912  pceu  12915  pcqmul  12922  pcqdiv  12926  f1ocpbllem  13442  funcoppc  13765  funcres  13786  catcisolem  13954  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  latjlej12  14189  latmlem12  14205  latj4  14223  latj4rot  14224  odcong  14880  cmn4  15124  ablsub4  15130  abladdsub4  15131  lsm4  15168  abvdom  15619  abvres  15620  abvtrivd  15621  lspsolvlem  15911  lbsextlem2  15928  nllyrest  17228  hausflimlem  17690  tsmsxp  17853  xmetlecl  17927  prdsxmetlem  17948  bndth  18472  cph2ass  18664  iscau3  18720  dvres2  19278  coemullem  19647  vieta1  19708  aalioulem4  19731  cxpcn3lem  20103  angcan  20116  dchrvmasumlema  20665  logdivsum  20698  abvcxp  20780  padicabv  20795  gxneg  20949  gxsuc  20955  gxmodid  20962  adjlnop  22682  xreceu  23121  measvunilem  23555  measvunilem0  23556  subdivcomb1  24105  subdivcomb2  24106  ax5seglem3  24631  ax5seglem6  24634  axpasch  24641  axeuclid  24663  axcontlem4  24667  axcontlem8  24671  cgrcomim  24684  cgrcoml  24691  cgrcomr  24692  cgrdegen  24699  segconeu  24706  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  btwnouttr  24719  btwnexch  24720  trisegint  24723  lineext  24771  linecgr  24776  lineid  24778  idinside  24779  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem7  24788  btwnconn1lem14  24795  btwnconn2  24797  midofsegid  24799  btwnoutside  24820  outsideoftr  24824  lineunray  24842  lineelsb2  24843  uninqs  25142  infxpg  25198  prltub  25363  mulinvsca  25583  truni3  25610  prdnei  25676  supnufb  25733  mulmulvec  25790  distsava  25792  vtarl  25990  cmpmorass  26069  cnres2  26586  heibor  26648  mzpsubst  26929  pellex  27023  pellfundex  27074  pellfund14gap  27075  qirropth  27096  rmxypos  27137  congmul  27157  congsub  27160  mzpcong  27162  coprmdvdsb  27177  jm2.15nn0  27199  jm2.16nn0  27200  rpnnen3lem  27227  symgsssg  27511  symgfisg  27512  psgnunilem4  27523  idomsubgmo  27617  stoweidlem57  27909  istrlon  28340  bnj1128  29336  lsmcv2  29841  lcvat  29842  lcvexchlem4  29849  lcvexchlem5  29850  lfladd  29878  lflsub  29879  lflmul  29880  lshpkrlem4  29925  latm4  30045  omlmod1i2N  30072  cvlatexch3  30150  cvlsupr7  30160  hlatj4  30185  hlrelat3  30223  cvrval3  30224  atcvrj1  30242  atlelt  30249  2atlt  30250  2atjm  30256  3noncolr2  30260  athgt  30267  3dimlem2  30270  3dimlem4  30275  3dimlem4OLDN  30276  3dim3  30280  1cvratex  30284  ps-1  30288  ps-2  30289  hlatexch3N  30291  llnle  30329  atcvrlln2  30330  atcvrlln  30331  lplni2  30348  lplnle  30351  lplnnle2at  30352  llncvrlpln2  30368  lplnexllnN  30375  2llnmeqat  30382  lvolnle3at  30393  4atlem0ae  30405  lplncvrlvol2  30426  lnjatN  30591  lncvrat  30593  cdlemblem  30604  elpaddri  30613  paddasslem2  30632  paddasslem16  30646  padd4N  30651  hlmod1i  30667  dalawlem2  30683  pclfinN  30711  pexmidlem4N  30784  pl42lem1N  30790  lhp2lt  30812  lhpexle1  30819  lhpexle2lem  30820  lhpj1  30833  lhpmcvr5N  30838  lhp2at0  30843  lhp2atnle  30844  lhp2at0nle  30846  lhple  30853  lhpat  30854  lhpat4N  30855  4atexlempnq  30866  4atexlem7  30886  4atex  30887  ltrn11  30937  ltrnle  30940  ltrnm  30942  ltrnj  30943  ltrncvr  30944  ltrnel  30950  ltrncnvel  30953  ltrncnv  30957  ltrnmw  30962  trlval2  30974  trlcnv  30976  trljat1  30977  trljat2  30978  trlat  30980  trl0  30981  trlnidat  30984  trlnid  30990  cdlemc1  31002  cdlemc2  31003  cdlemc5  31006  cdlemd2  31010  cdlemd7  31015  cdlemd8  31016  cdlemd9  31017  cdleme0e  31028  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme5  31051  cdleme10  31065  cdleme11a  31071  cdleme11c  31072  cdleme11h  31077  cdleme11j  31078  cdleme0nex  31101  cdleme18a  31102  cdleme18b  31103  cdleme22gb  31105  cdleme20zN  31112  cdleme20y  31113  cdleme20c  31122  cdleme20k  31130  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme21h  31145  cdleme22b  31152  cdleme22d  31154  cdleme22f  31157  cdleme25a  31164  cdleme25c  31166  cdleme25dN  31167  cdleme26ee  31171  cdleme30a  31189  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdleme43fsv1snlem  31231  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdlemefs31fv1  31235  cdleme36a  31271  cdleme39a  31276  cdleme42a  31282  cdleme42c  31283  cdleme17d3  31307  cdleme48fv  31310  cdleme48bw  31313  cdleme48b  31314  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdleme48d  31346  cdleme50trn2a  31361  cdleme50trn2  31362  cdleme50ltrn  31368  cdlemf1  31372  cdlemf  31374  trlord  31380  cdlemg2dN  31401  cdlemg2fvlem  31405  cdlemg2l  31414  cdlemg7fvbwN  31418  cdlemg7aN  31436  cdlemg10bALTN  31447  cdlemg10c  31450  cdlemg17a  31472  cdlemg17dALTN  31475  cdlemg31b0a  31506  cdlemg31a  31508  cdlemg31b  31509  cdlemg34  31523  cdlemg36  31525  ltrnco  31530  trlcoabs2N  31533  trlcolem  31537  cdlemg48  31548  tgrpov  31559  tendoco2  31579  tendoplco2  31590  cdlemh1  31626  cdlemi1  31629  cdlemi2  31630  cdlemj3  31634  tendoid0  31636  cdlemk1  31642  cdlemk2  31643  cdlemk4  31645  cdlemk8  31649  cdlemk9  31650  cdlemk9bN  31651  cdlemk10  31654  cdlemk26b-3  31716  cdlemk26-3  31717  cdlemk28-3  31719  cdlemk37  31725  cdlemk39  31727  cdlemkfid1N  31732  cdlemkid1  31733  cdlemky  31737  cdlemkyu  31738  cdlemk19ylem  31741  cdlemk19xlem  31753  cdlemk11t  31757  cdlemk51  31764  cdlemkyyN  31773  cdleml6  31792  cdleml7  31793  cdleml8  31794  cdleml9  31795  erngdvlem4  31802  erngdvlem4-rN  31810  tendospcanN  31835  dia11N  31860  cdlemm10N  31930  dib11N  31972  dicvaddcl  32002  dicvscacl  32003  cdlemn6  32014  dihvalcq2  32059  dihopelvalcpre  32060  dihord6b  32072  dihord5apre  32074  dihmeetlem1N  32102  dihmeetlem2N  32111  dihglbcpreN  32112  dihjatc1  32123  dihmeetlem20N  32138  dih1dimatlem0  32140  dihatlat  32146  dihglblem6  32152  dochexmidlem4  32275  mapdpglem32  32517  mapdh8ad  32591  mapdh9aOLDN  32603  hdmap11lem2  32657  hdmap14lem6  32688
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