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

Theorem simp3l 1034
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 1029 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 985
This theorem is referenced by:  simpl3l  1061  simpr3l  1067  simp13l  1121  simp23l  1127  simp33l  1133  disjss3  4420  tfisi  6697  tfrlem5  7104  omeulem1  7289  omeulem2  7290  uniinqs  7449  elfiun  7948  tcrank  8358  isfin2-2  8751  konigthlem  8995  gruen  9239  addid2  9818  mulcan  10251  mulcan2  10252  divass  10290  divdir  10295  div11  10298  divcan5  10311  ltmul1  10457  ltdiv1  10471  ltmuldiv  10480  lediv2  10498  xaddass2  11538  xlt2add  11548  xmulasslem3  11574  xadddi2  11585  expaddz  12317  expmulz  12319  resqrtcl  13311  o1add  13670  o1mul  13671  o1sub  13672  dvdsadd2b  14340  dvdsgcd  14504  rpexp12i  14667  pythagtriplem3  14761  pcpremul  14786  pceu  14789  pcqmul  14796  pcqdiv  14800  f1ocpbllem  15423  funcoppc  15773  funcres  15794  catcisolem  15994  1stfcl  16075  2ndfcl  16076  prfcl  16081  evlfcl  16100  curf1cl  16106  curfcl  16110  hofcl  16137  latjlej12  16306  latmlem12  16322  latj4  16340  latj4rot  16341  symgsssg  17101  symgfisg  17102  psgnunilem4  17131  odcong  17191  cmn4  17442  ablsub4  17448  abladdsub4  17449  lsm4  17491  abvdom  18059  abvres  18060  abvtrivd  18061  lspsolvlem  18358  lbsextlem2  18375  lidlsubcl  18432  frlmbas3  19326  matmulcell  19462  marrepeval  19580  ma1repveval  19588  submaeval  19599  mdetunilem3  19631  mdetuni0  19638  mdetmul  19640  minmar1eval  19666  nllyrest  20493  hausflimlem  20986  tsmsxp  21161  psmetlecl  21323  xmetlecl  21353  prdsxmetlem  21375  bndth  21978  cph2ass  22182  iscau3  22240  dvres2  22859  coemullem  23196  vieta1  23257  aalioulem4  23283  cxpcn3lem  23679  angcan  23723  dchrvmasumlema  24330  logdivsum  24363  abvcxp  24445  padicabv  24460  ax5seglem3  24953  ax5seglem6  24956  axpasch  24963  axeuclid  24985  axcontlem4  24989  axcontlem8  24993  clwwlknimp  25496  gxneg  25986  gxsuc  25992  gxmodid  25999  adjlnop  27731  xreceu  28392  orngmul  28568  rhmdvd  28586  measvunilem  29036  measvunilem0  29037  measres  29046  bnj1128  29801  subdivcomb1  30361  subdivcomb2  30362  cgrcomim  30755  cgrcoml  30762  cgrcomr  30763  cgrdegen  30770  segconeu  30777  btwnintr  30785  btwnexch3  30786  btwnouttr2  30788  btwnouttr  30790  btwnexch  30791  trisegint  30794  lineext  30842  linecgr  30847  lineid  30849  idinside  30850  btwnconn1lem3  30855  btwnconn1lem4  30856  btwnconn1lem7  30859  btwnconn1lem14  30866  btwnconn2  30868  midofsegid  30870  btwnoutside  30891  outsideoftr  30895  lineunray  30913  lineelsb2  30914  cnres2  32053  heibor  32111  lsmcv2  32558  lcvat  32559  lcvexchlem4  32566  lcvexchlem5  32567  lfladd  32595  lflsub  32596  lflmul  32597  lshpkrlem4  32642  latm4  32762  omlmod1i2N  32789  cvlatexch3  32867  cvlsupr7  32877  hlatj4  32902  hlrelat3  32940  cvrval3  32941  atcvrj1  32959  atlelt  32966  2atlt  32967  2atjm  32973  3noncolr2  32977  athgt  32984  3dimlem2  32987  3dimlem4  32992  3dimlem4OLDN  32993  3dim3  32997  1cvratex  33001  ps-1  33005  ps-2  33006  hlatexch3N  33008  llnle  33046  atcvrlln2  33047  atcvrlln  33048  lplni2  33065  lplnle  33068  lplnnle2at  33069  llncvrlpln2  33085  lplnexllnN  33092  2llnmeqat  33099  lvolnle3at  33110  4atlem0ae  33122  lplncvrlvol2  33143  lnjatN  33308  lncvrat  33310  cdlemblem  33321  elpaddri  33330  paddasslem2  33349  paddasslem16  33363  padd4N  33368  hlmod1i  33384  dalawlem2  33400  pclfinN  33428  pexmidlem4N  33501  pl42lem1N  33507  lhp2lt  33529  lhpexle1  33536  lhpexle2lem  33537  lhpj1  33550  lhpmcvr5N  33555  lhp2at0  33560  lhp2atnle  33561  lhp2at0nle  33563  lhple  33570  lhpat  33571  lhpat4N  33572  4atexlempnq  33583  4atexlem7  33603  4atex  33604  ltrn11  33654  ltrnle  33657  ltrnm  33659  ltrnj  33660  ltrncvr  33661  ltrnel  33667  ltrncnvel  33670  ltrncnv  33674  ltrnmwOLD  33680  trlval2  33692  trlcnv  33694  trljat1  33695  trljat2  33696  trlat  33698  trl0  33699  trlnidat  33702  trlnid  33708  cdlemc1  33720  cdlemc2  33721  cdlemc5  33724  cdlemd2  33728  cdlemd7  33733  cdlemd8  33734  cdlemd9  33735  cdleme0e  33746  cdleme3g  33763  cdleme3h  33764  cdleme3  33766  cdleme5  33769  cdleme10  33783  cdleme11a  33789  cdleme11c  33790  cdleme11h  33795  cdleme11j  33796  cdleme0nex  33819  cdleme18a  33820  cdleme18b  33821  cdleme22gb  33823  cdleme20zN  33830  cdleme20yOLD  33832  cdleme20c  33841  cdleme20k  33849  cdleme21a  33855  cdleme21b  33856  cdleme21c  33857  cdleme21h  33864  cdleme22b  33871  cdleme22d  33873  cdleme22f  33876  cdleme25a  33883  cdleme25c  33885  cdleme25dN  33886  cdleme26ee  33890  cdleme30a  33908  cdlemefr29bpre0N  33936  cdlemefr29clN  33937  cdlemefr32fvaN  33939  cdlemefr32fva1  33940  cdlemefs29bpre0N  33946  cdlemefs29bpre1N  33947  cdlemefs29cpre1N  33948  cdlemefs29clN  33949  cdleme43fsv1snlem  33950  cdlemefs32fvaN  33952  cdlemefs32fva1  33953  cdlemefs31fv1  33954  cdleme36a  33990  cdleme39a  33995  cdleme42a  34001  cdleme42c  34002  cdleme17d3  34026  cdleme48fv  34029  cdleme48bw  34032  cdleme48b  34033  cdlemeg46rgv  34058  cdlemeg46req  34059  cdlemeg46gfv  34060  cdleme48d  34065  cdleme50trn2a  34080  cdleme50trn2  34081  cdleme50ltrn  34087  cdlemf1  34091  cdlemf  34093  trlord  34099  cdlemg2dN  34120  cdlemg2fvlem  34124  cdlemg2l  34133  cdlemg7fvbwN  34137  cdlemg7aN  34155  cdlemg10bALTN  34166  cdlemg10c  34169  cdlemg17a  34191  cdlemg17dALTN  34194  cdlemg31b0a  34225  cdlemg31a  34227  cdlemg31b  34228  cdlemg34  34242  cdlemg36  34244  ltrnco  34249  trlcoabs2N  34252  trlcolem  34256  cdlemg48  34267  tgrpov  34278  tendoco2  34298  tendoplco2  34309  cdlemh1  34345  cdlemi1  34348  cdlemi2  34349  cdlemj3  34353  tendoid0  34355  cdlemk1  34361  cdlemk2  34362  cdlemk4  34364  cdlemk8  34368  cdlemk9  34369  cdlemk9bN  34370  cdlemk10  34373  cdlemk26b-3  34435  cdlemk26-3  34436  cdlemk28-3  34438  cdlemk37  34444  cdlemk39  34446  cdlemkfid1N  34451  cdlemkid1  34452  cdlemky  34456  cdlemkyu  34457  cdlemk19ylem  34460  cdlemk19xlem  34472  cdlemk11t  34476  cdlemk51  34483  cdlemkyyN  34492  cdleml6  34511  cdleml7  34512  cdleml8  34513  cdleml9  34514  erngdvlem4  34521  erngdvlem4-rN  34529  tendospcanN  34554  dia11N  34579  cdlemm10N  34649  dib11N  34691  dicvaddcl  34721  dicvscacl  34722  cdlemn6  34733  dihvalcq2  34778  dihopelvalcpre  34779  dihord6b  34791  dihord5apre  34793  dihmeetlem1N  34821  dihmeetlem2N  34830  dihglbcpreN  34831  dihjatc1  34842  dihmeetlem20N  34857  dih1dimatlem0  34859  dihatlat  34865  dihglblem6  34871  dochexmidlem4  34994  mapdpglem32  35236  mapdh8ad  35310  mapdh9aOLDN  35322  hdmap11lem2  35376  hdmap14lem6  35407  mzpsubst  35553  pellex  35643  pellfundex  35698  pellfund14gap  35699  qirropth  35720  rmxypos  35761  congmul  35781  congsub  35784  mzpcong  35786  coprmdvdsb  35801  jm2.15nn0  35822  jm2.16nn0  35823  rpnnen3lem  35850  idomsubgmo  36036  relexp01min  36209  mullimc  37560  islptre  37563  limccog  37564  mullimcf  37567  addlimc  37593  0ellimcdiv  37594  stoweidlem57  37782  fourierdlem48  37882  fourierdlem80  37914  fourierdlem113  37947  ovncvrrp  38205
  Copyright terms: Public domain W3C validator