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

Theorem simp3l 986
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 445 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 981 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpl3l  1013  simpr3l  1019  simp13l  1073  simp23l  1079  simp33l  1085  disjss3  4236  tfisi  4867  omeulem1  6854  omeulem2  6855  uniinqs  7013  elfiun  7464  tcrank  7839  isfin2-2  8230  konigthlem  8474  gruen  8718  addid2  9280  mulcan  9690  mulcan2  9691  divass  9727  divdir  9732  div11  9735  divcan5  9747  ltmul1  9891  ltdiv1  9905  ltmuldiv  9911  lediv2  9931  xaddass2  10860  xlt2add  10870  xmulasslem3  10896  xadddi2  10907  expaddz  11455  expmulz  11457  resqrcl  12090  o1add  12438  o1mul  12439  o1sub  12440  dvdsadd2b  12923  dvdsgcd  13074  rpexp12i  13153  pythagtriplem3  13223  pcpremul  13248  pceu  13251  pcqmul  13258  pcqdiv  13262  f1ocpbllem  13780  funcoppc  14103  funcres  14124  catcisolem  14292  1stfcl  14325  2ndfcl  14326  prfcl  14331  evlfcl  14350  curf1cl  14356  curfcl  14360  hofcl  14387  latjlej12  14527  latmlem12  14543  latj4  14561  latj4rot  14562  odcong  15218  cmn4  15462  ablsub4  15468  abladdsub4  15469  lsm4  15506  abvdom  15957  abvres  15958  abvtrivd  15959  lspsolvlem  16245  lbsextlem2  16262  nllyrest  17580  hausflimlem  18042  tsmsxp  18215  psmetlecl  18377  xmetlecl  18407  prdsxmetlem  18429  bndth  19014  cph2ass  19206  iscau3  19262  dvres2  19830  coemullem  20199  vieta1  20260  aalioulem4  20283  cxpcn3lem  20662  angcan  20675  dchrvmasumlema  21225  logdivsum  21258  abvcxp  21340  padicabv  21355  gxneg  21885  gxsuc  21891  gxmodid  21898  adjlnop  23620  xreceu  24199  rhmdvd  24290  measvunilem  24597  measvunilem0  24598  measres  24607  subdivcomb1  25226  subdivcomb2  25227  ax5seglem3  25901  ax5seglem6  25904  axpasch  25911  axeuclid  25933  axcontlem4  25937  axcontlem8  25941  cgrcomim  25954  cgrcoml  25961  cgrcomr  25962  cgrdegen  25969  segconeu  25976  btwnintr  25984  btwnexch3  25985  btwnouttr2  25987  btwnouttr  25989  btwnexch  25990  trisegint  25993  lineext  26041  linecgr  26046  lineid  26048  idinside  26049  btwnconn1lem3  26054  btwnconn1lem4  26055  btwnconn1lem7  26058  btwnconn1lem14  26065  btwnconn2  26067  midofsegid  26069  btwnoutside  26090  outsideoftr  26094  lineunray  26112  lineelsb2  26113  cnres2  26510  heibor  26568  mzpsubst  26843  pellex  26936  pellfundex  26987  pellfund14gap  26988  qirropth  27009  rmxypos  27050  congmul  27070  congsub  27073  mzpcong  27075  coprmdvdsb  27090  jm2.15nn0  27112  jm2.16nn0  27113  rpnnen3lem  27140  symgsssg  27423  symgfisg  27424  psgnunilem4  27435  idomsubgmo  27529  stoweidlem57  27820  bnj1128  29457  lsmcv2  29925  lcvat  29926  lcvexchlem4  29933  lcvexchlem5  29934  lfladd  29962  lflsub  29963  lflmul  29964  lshpkrlem4  30009  latm4  30129  omlmod1i2N  30156  cvlatexch3  30234  cvlsupr7  30244  hlatj4  30269  hlrelat3  30307  cvrval3  30308  atcvrj1  30326  atlelt  30333  2atlt  30334  2atjm  30340  3noncolr2  30344  athgt  30351  3dimlem2  30354  3dimlem4  30359  3dimlem4OLDN  30360  3dim3  30364  1cvratex  30368  ps-1  30372  ps-2  30373  hlatexch3N  30375  llnle  30413  atcvrlln2  30414  atcvrlln  30415  lplni2  30432  lplnle  30435  lplnnle2at  30436  llncvrlpln2  30452  lplnexllnN  30459  2llnmeqat  30466  lvolnle3at  30477  4atlem0ae  30489  lplncvrlvol2  30510  lnjatN  30675  lncvrat  30677  cdlemblem  30688  elpaddri  30697  paddasslem2  30716  paddasslem16  30730  padd4N  30735  hlmod1i  30751  dalawlem2  30767  pclfinN  30795  pexmidlem4N  30868  pl42lem1N  30874  lhp2lt  30896  lhpexle1  30903  lhpexle2lem  30904  lhpj1  30917  lhpmcvr5N  30922  lhp2at0  30927  lhp2atnle  30928  lhp2at0nle  30930  lhple  30937  lhpat  30938  lhpat4N  30939  4atexlempnq  30950  4atexlem7  30970  4atex  30971  ltrn11  31021  ltrnle  31024  ltrnm  31026  ltrnj  31027  ltrncvr  31028  ltrnel  31034  ltrncnvel  31037  ltrncnv  31041  ltrnmw  31046  trlval2  31058  trlcnv  31060  trljat1  31061  trljat2  31062  trlat  31064  trl0  31065  trlnidat  31068  trlnid  31074  cdlemc1  31086  cdlemc2  31087  cdlemc5  31090  cdlemd2  31094  cdlemd7  31099  cdlemd8  31100  cdlemd9  31101  cdleme0e  31112  cdleme3g  31129  cdleme3h  31130  cdleme3  31132  cdleme5  31135  cdleme10  31149  cdleme11a  31155  cdleme11c  31156  cdleme11h  31161  cdleme11j  31162  cdleme0nex  31185  cdleme18a  31186  cdleme18b  31187  cdleme22gb  31189  cdleme20zN  31196  cdleme20y  31197  cdleme20c  31206  cdleme20k  31214  cdleme21a  31220  cdleme21b  31221  cdleme21c  31222  cdleme21h  31229  cdleme22b  31236  cdleme22d  31238  cdleme22f  31241  cdleme25a  31248  cdleme25c  31250  cdleme25dN  31251  cdleme26ee  31255  cdleme30a  31273  cdlemefr29bpre0N  31301  cdlemefr29clN  31302  cdlemefr32fvaN  31304  cdlemefr32fva1  31305  cdlemefs29bpre0N  31311  cdlemefs29bpre1N  31312  cdlemefs29cpre1N  31313  cdlemefs29clN  31314  cdleme43fsv1snlem  31315  cdlemefs32fvaN  31317  cdlemefs32fva1  31318  cdlemefs31fv1  31319  cdleme36a  31355  cdleme39a  31360  cdleme42a  31366  cdleme42c  31367  cdleme17d3  31391  cdleme48fv  31394  cdleme48bw  31397  cdleme48b  31398  cdlemeg46rgv  31423  cdlemeg46req  31424  cdlemeg46gfv  31425  cdleme48d  31430  cdleme50trn2a  31445  cdleme50trn2  31446  cdleme50ltrn  31452  cdlemf1  31456  cdlemf  31458  trlord  31464  cdlemg2dN  31485  cdlemg2fvlem  31489  cdlemg2l  31498  cdlemg7fvbwN  31502  cdlemg7aN  31520  cdlemg10bALTN  31531  cdlemg10c  31534  cdlemg17a  31556  cdlemg17dALTN  31559  cdlemg31b0a  31590  cdlemg31a  31592  cdlemg31b  31593  cdlemg34  31607  cdlemg36  31609  ltrnco  31614  trlcoabs2N  31617  trlcolem  31621  cdlemg48  31632  tgrpov  31643  tendoco2  31663  tendoplco2  31674  cdlemh1  31710  cdlemi1  31713  cdlemi2  31714  cdlemj3  31718  tendoid0  31720  cdlemk1  31726  cdlemk2  31727  cdlemk4  31729  cdlemk8  31733  cdlemk9  31734  cdlemk9bN  31735  cdlemk10  31738  cdlemk26b-3  31800  cdlemk26-3  31801  cdlemk28-3  31803  cdlemk37  31809  cdlemk39  31811  cdlemkfid1N  31816  cdlemkid1  31817  cdlemky  31821  cdlemkyu  31822  cdlemk19ylem  31825  cdlemk19xlem  31837  cdlemk11t  31841  cdlemk51  31848  cdlemkyyN  31857  cdleml6  31876  cdleml7  31877  cdleml8  31878  cdleml9  31879  erngdvlem4  31886  erngdvlem4-rN  31894  tendospcanN  31919  dia11N  31944  cdlemm10N  32014  dib11N  32056  dicvaddcl  32086  dicvscacl  32087  cdlemn6  32098  dihvalcq2  32143  dihopelvalcpre  32144  dihord6b  32156  dihord5apre  32158  dihmeetlem1N  32186  dihmeetlem2N  32195  dihglbcpreN  32196  dihjatc1  32207  dihmeetlem20N  32222  dih1dimatlem0  32224  dihatlat  32230  dihglblem6  32236  dochexmidlem4  32359  mapdpglem32  32601  mapdh8ad  32675  mapdh9aOLDN  32687  hdmap11lem2  32741  hdmap14lem6  32772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator