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

Theorem simp3l 1037
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 459 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1032 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 986
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 189  df-an 373  df-3an 988
This theorem is referenced by:  simpl3l  1064  simpr3l  1070  simp13l  1124  simp23l  1130  simp33l  1136  disjss3  4404  tfisi  6690  tfrlem5  7103  omeulem1  7288  omeulem2  7289  uniinqs  7448  elfiun  7949  tcrank  8360  isfin2-2  8754  konigthlem  8998  gruen  9242  addid2  9821  mulcan  10256  mulcan2  10257  divass  10295  divdir  10300  div11  10303  divcan5  10316  ltmul1  10462  ltdiv1  10476  ltmuldiv  10485  lediv2  10503  xaddass2  11543  xlt2add  11553  xmulasslem3  11579  xadddi2  11590  expaddz  12323  expmulz  12325  resqrtcl  13329  o1add  13689  o1mul  13690  o1sub  13691  dvdsadd2b  14359  dvdsgcd  14523  rpexp12i  14686  pythagtriplem3  14780  pcpremul  14805  pceu  14808  pcqmul  14815  pcqdiv  14819  f1ocpbllem  15442  funcoppc  15792  funcres  15813  catcisolem  16013  1stfcl  16094  2ndfcl  16095  prfcl  16100  evlfcl  16119  curf1cl  16125  curfcl  16129  hofcl  16156  latjlej12  16325  latmlem12  16341  latj4  16359  latj4rot  16360  symgsssg  17120  symgfisg  17121  psgnunilem4  17150  odcong  17210  cmn4  17461  ablsub4  17467  abladdsub4  17468  lsm4  17510  abvdom  18078  abvres  18079  abvtrivd  18080  lspsolvlem  18377  lbsextlem2  18394  lidlsubcl  18451  frlmbas3  19346  matmulcell  19482  marrepeval  19600  ma1repveval  19608  submaeval  19619  mdetunilem3  19651  mdetuni0  19658  mdetmul  19660  minmar1eval  19686  nllyrest  20513  hausflimlem  21006  tsmsxp  21181  psmetlecl  21343  xmetlecl  21373  prdsxmetlem  21395  bndth  21998  cph2ass  22202  iscau3  22260  dvres2  22879  coemullem  23216  vieta1  23277  aalioulem4  23303  cxpcn3lem  23699  angcan  23743  dchrvmasumlema  24350  logdivsum  24383  abvcxp  24465  padicabv  24480  ax5seglem3  24973  ax5seglem6  24976  axpasch  24983  axeuclid  25005  axcontlem4  25009  axcontlem8  25013  clwwlknimp  25516  gxneg  26006  gxsuc  26012  gxmodid  26019  adjlnop  27751  xreceu  28403  orngmul  28578  rhmdvd  28596  measvunilem  29046  measvunilem0  29047  measres  29056  bnj1128  29811  subdivcomb1  30372  subdivcomb2  30373  cgrcomim  30768  cgrcoml  30775  cgrcomr  30776  cgrdegen  30783  segconeu  30790  btwnintr  30798  btwnexch3  30799  btwnouttr2  30801  btwnouttr  30803  btwnexch  30804  trisegint  30807  lineext  30855  linecgr  30860  lineid  30862  idinside  30863  btwnconn1lem3  30868  btwnconn1lem4  30869  btwnconn1lem7  30872  btwnconn1lem14  30879  btwnconn2  30881  midofsegid  30883  btwnoutside  30904  outsideoftr  30908  lineunray  30926  lineelsb2  30927  cnres2  32107  heibor  32165  lsmcv2  32607  lcvat  32608  lcvexchlem4  32615  lcvexchlem5  32616  lfladd  32644  lflsub  32645  lflmul  32646  lshpkrlem4  32691  latm4  32811  omlmod1i2N  32838  cvlatexch3  32916  cvlsupr7  32926  hlatj4  32951  hlrelat3  32989  cvrval3  32990  atcvrj1  33008  atlelt  33015  2atlt  33016  2atjm  33022  3noncolr2  33026  athgt  33033  3dimlem2  33036  3dimlem4  33041  3dimlem4OLDN  33042  3dim3  33046  1cvratex  33050  ps-1  33054  ps-2  33055  hlatexch3N  33057  llnle  33095  atcvrlln2  33096  atcvrlln  33097  lplni2  33114  lplnle  33117  lplnnle2at  33118  llncvrlpln2  33134  lplnexllnN  33141  2llnmeqat  33148  lvolnle3at  33159  4atlem0ae  33171  lplncvrlvol2  33192  lnjatN  33357  lncvrat  33359  cdlemblem  33370  elpaddri  33379  paddasslem2  33398  paddasslem16  33412  padd4N  33417  hlmod1i  33433  dalawlem2  33449  pclfinN  33477  pexmidlem4N  33550  pl42lem1N  33556  lhp2lt  33578  lhpexle1  33585  lhpexle2lem  33586  lhpj1  33599  lhpmcvr5N  33604  lhp2at0  33609  lhp2atnle  33610  lhp2at0nle  33612  lhple  33619  lhpat  33620  lhpat4N  33621  4atexlempnq  33632  4atexlem7  33652  4atex  33653  ltrn11  33703  ltrnle  33706  ltrnm  33708  ltrnj  33709  ltrncvr  33710  ltrnel  33716  ltrncnvel  33719  ltrncnv  33723  ltrnmwOLD  33729  trlval2  33741  trlcnv  33743  trljat1  33744  trljat2  33745  trlat  33747  trl0  33748  trlnidat  33751  trlnid  33757  cdlemc1  33769  cdlemc2  33770  cdlemc5  33773  cdlemd2  33777  cdlemd7  33782  cdlemd8  33783  cdlemd9  33784  cdleme0e  33795  cdleme3g  33812  cdleme3h  33813  cdleme3  33815  cdleme5  33818  cdleme10  33832  cdleme11a  33838  cdleme11c  33839  cdleme11h  33844  cdleme11j  33845  cdleme0nex  33868  cdleme18a  33869  cdleme18b  33870  cdleme22gb  33872  cdleme20zN  33879  cdleme20yOLD  33881  cdleme20c  33890  cdleme20k  33898  cdleme21a  33904  cdleme21b  33905  cdleme21c  33906  cdleme21h  33913  cdleme22b  33920  cdleme22d  33922  cdleme22f  33925  cdleme25a  33932  cdleme25c  33934  cdleme25dN  33935  cdleme26ee  33939  cdleme30a  33957  cdlemefr29bpre0N  33985  cdlemefr29clN  33986  cdlemefr32fvaN  33988  cdlemefr32fva1  33989  cdlemefs29bpre0N  33995  cdlemefs29bpre1N  33996  cdlemefs29cpre1N  33997  cdlemefs29clN  33998  cdleme43fsv1snlem  33999  cdlemefs32fvaN  34001  cdlemefs32fva1  34002  cdlemefs31fv1  34003  cdleme36a  34039  cdleme39a  34044  cdleme42a  34050  cdleme42c  34051  cdleme17d3  34075  cdleme48fv  34078  cdleme48bw  34081  cdleme48b  34082  cdlemeg46rgv  34107  cdlemeg46req  34108  cdlemeg46gfv  34109  cdleme48d  34114  cdleme50trn2a  34129  cdleme50trn2  34130  cdleme50ltrn  34136  cdlemf1  34140  cdlemf  34142  trlord  34148  cdlemg2dN  34169  cdlemg2fvlem  34173  cdlemg2l  34182  cdlemg7fvbwN  34186  cdlemg7aN  34204  cdlemg10bALTN  34215  cdlemg10c  34218  cdlemg17a  34240  cdlemg17dALTN  34243  cdlemg31b0a  34274  cdlemg31a  34276  cdlemg31b  34277  cdlemg34  34291  cdlemg36  34293  ltrnco  34298  trlcoabs2N  34301  trlcolem  34305  cdlemg48  34316  tgrpov  34327  tendoco2  34347  tendoplco2  34358  cdlemh1  34394  cdlemi1  34397  cdlemi2  34398  cdlemj3  34402  tendoid0  34404  cdlemk1  34410  cdlemk2  34411  cdlemk4  34413  cdlemk8  34417  cdlemk9  34418  cdlemk9bN  34419  cdlemk10  34422  cdlemk26b-3  34484  cdlemk26-3  34485  cdlemk28-3  34487  cdlemk37  34493  cdlemk39  34495  cdlemkfid1N  34500  cdlemkid1  34501  cdlemky  34505  cdlemkyu  34506  cdlemk19ylem  34509  cdlemk19xlem  34521  cdlemk11t  34525  cdlemk51  34532  cdlemkyyN  34541  cdleml6  34560  cdleml7  34561  cdleml8  34562  cdleml9  34563  erngdvlem4  34570  erngdvlem4-rN  34578  tendospcanN  34603  dia11N  34628  cdlemm10N  34698  dib11N  34740  dicvaddcl  34770  dicvscacl  34771  cdlemn6  34782  dihvalcq2  34827  dihopelvalcpre  34828  dihord6b  34840  dihord5apre  34842  dihmeetlem1N  34870  dihmeetlem2N  34879  dihglbcpreN  34880  dihjatc1  34891  dihmeetlem20N  34906  dih1dimatlem0  34908  dihatlat  34914  dihglblem6  34920  dochexmidlem4  35043  mapdpglem32  35285  mapdh8ad  35359  mapdh9aOLDN  35371  hdmap11lem2  35425  hdmap14lem6  35456  mzpsubst  35602  pellex  35691  pellfundex  35746  pellfund14gap  35747  qirropth  35768  rmxypos  35809  congmul  35829  congsub  35832  mzpcong  35834  coprmdvdsb  35849  jm2.15nn0  35870  jm2.16nn0  35871  rpnnen3lem  35898  idomsubgmo  36084  relexp01min  36317  mullimc  37706  islptre  37709  limccog  37710  mullimcf  37713  addlimc  37739  0ellimcdiv  37740  stoweidlem57  37928  fourierdlem48  38028  fourierdlem80  38060  fourierdlem113  38093  ovncvrrp  38396  opnvonmbllem2  38465  trlsonwlkon  39688
  Copyright terms: Public domain W3C validator