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

Theorem simp3d 1010
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp3d  |-  ( ph  ->  th )

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp3 998 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  simp3bi  1013  f1dom3fv3dif  6161  f1dom3el3dif  6162  oeeui  7248  erinxp  7382  resixp  7501  domssex2  7674  cantnflem1c  8102  cantnflem1  8104  cantnflem3  8106  cantnflem4  8107  cantnflem1cOLD  8125  cantnflem1OLD  8127  cantnflem3OLD  8128  cantnflem4OLD  8129  fpwwe2lem7  9010  canthnumlem  9022  canthp1lem2  9027  wununi  9080  wunpw  9081  wunpr  9083  ixxdisj  11540  ixxun  11541  ixxss1  11543  ixxss2  11544  ixxss12  11545  ixxub  11546  ixxlb  11547  lbioo  11556  iccsupr  11613  icodisj  11641  xov1plusxeqvd  11662  supicc  11664  intfracq  11950  fldiv  11951  seqf1olem2  12111  cjmul  12934  icco1  13322  rpnnen2lem10  13814  ruclem2  13822  ruclem3  13823  ruclem9  13828  ruclem12  13831  dvdslegcd  14009  crt  14163  eulerthlem1  14166  eulerthlem2  14167  pcpremul  14222  prmreclem2  14290  prmreclem3  14291  4sqlem13  14330  sectcan  15007  sectco  15008  sectmon  15029  monsect  15030  funcid  15093  funcco  15094  funcsect  15095  invfuc  15197  fuciso  15198  coapm  15252  catciso  15288  postr  15436  ipodrsima  15648  psref2  15687  psasym  15693  mhm0  15785  submcl  15794  submmnd  15795  eqger  16046  eqgcpbl  16050  gaorber  16141  orbsta  16146  cayleyth  16235  pmtrrn2  16281  pmtrfinv  16282  pmtrfmvdn0  16283  dfod2  16382  sylow2blem1  16436  sylow2blem3  16438  dprdcntz  16832  dprddisj  16833  dprdffsupp  16838  dprdffiOLD  16844  dpjdisj  16892  ablfac1a  16910  ablfac1b  16911  rngsrg  17024  lmodvsdir  17319  lmhmlin  17464  lbsind  17509  2idlcpbl  17664  assasca  17741  mpfind  17976  mpt2frlmd  18575  mdetunilem2  18882  mdetunilem5  18885  mdetunilem6  18886  mnfnei  19488  cnprcl  19512  lmcvg  19529  lmff  19568  lmcls  19569  lmcnp  19571  fbasssin  20072  flimfil  20205  tgpconcomp  20346  tlmtrg  20427  ustssel  20443  ustincl  20445  ustdiag  20446  ustinvel  20447  ustexhalf  20448  ustfilxp  20450  tustopn  20509  tususp  20510  imasdsf1olem  20611  xmeter  20671  xmetresbl  20675  tmstopn  20723  metustexhalfOLD  20801  metustexhalf  20802  nlmnrg  20923  qdensere  21012  blcvx  21038  tgqioo  21040  icccmplem1  21062  icccmplem2  21063  reconnlem1  21066  cnmpt2pc  21163  iccpnfcnv  21179  phtpcer  21230  phtpcco2  21234  pcohtpy  21255  pcorev2  21263  pcophtb  21264  om1addcl  21268  pi1blem  21274  pi1cpbl  21279  pi1grplem  21284  pi1inv  21287  pi1xfrf  21288  pi1xfr  21290  pi1xfrcnvlem  21291  pi1cof  21294  pi1coghm  21296  cphreccllem  21360  cphsca  21361  cphsubrg  21362  cphsqrtcl2  21368  tchclm  21410  tchcph  21415  lmmcvg  21435  cmetcaulem  21462  lmcau  21486  bcthlem3  21500  bcthlem4  21501  minveclem4c  21575  minveclem2  21576  minveclem3b  21578  minveclem4  21582  minveclem6  21584  ivthicc  21605  ovollb2lem  21634  ovolshftlem1  21655  ovolscalem1  21659  ovolicc1  21662  ovolicc2lem2  21664  ovolicc2lem3  21665  ovolicc2lem4  21666  ovolicc2lem5  21667  ioombl1lem1  21703  dyadmaxlem  21741  volivth  21751  vitalilem2  21753  vitalilem4  21755  i1fima2  21821  itg2monolem1  21892  itgcnlem  21931  itgrevallem1  21936  itgreval  21938  itgle  21951  ibladd  21962  iblabslem  21969  itgspliticc  21978  itgsplitioo  21979  ditgcl  21997  ditgswap  21998  ditgsplitlem  21999  limcdif  22015  limcresi  22024  limcres  22025  limccnp  22030  limccnp2  22031  limcun  22034  dvlip  22129  dvlip2  22131  dveq0  22136  dvgt0lem1  22138  dvivthlem1  22144  dvcnvrelem1  22153  dvcnvre  22155  dvfsumlem2  22163  ftc1lem1  22171  ftc1lem2  22172  ftc1a  22173  ftc1lem4  22175  ftc2  22180  ftc2ditglem  22181  itgsubstlem  22184  ply1rem  22299  fta1glem2  22302  ig1pdvds  22312  plyrem  22435  fta1lem  22437  vieta1lem2  22441  aaliou3lem3  22474  pserulm  22551  psercnlem2  22553  psercnlem1  22554  psercn  22555  pserdvlem1  22556  pserdvlem2  22557  abelth2  22571  coseq00topi  22628  coseq0negpitopi  22629  cosordlem  22651  tanord1  22657  efif1olem1  22662  dvloglem  22757  efopnlem1  22765  logreclem  22878  chordthmlem4  22894  quart1  22915  quartlem2  22917  quartlem3  22918  quart  22920  acosbnd  22959  atancj  22969  atanlogsublem  22974  atantan  22982  atanbndlem  22984  atans2  22990  dvatan  22994  atantayl  22996  divsqrtsumlem  23037  ftalem5  23078  basellem5  23086  ppisval  23105  chtleppi  23213  chpchtsum  23222  chpub  23223  mersenne  23230  perfectlem2  23233  dchrinv  23264  rplogsumlem2  23398  chpdifbndlem1  23466  pntibndlem2  23504  pntlema  23509  pntlemb  23510  pntlemg  23511  pntlemh  23512  pntlemr  23515  pntlemj  23516  pntlemf  23518  pntlemk  23519  pntlemo  23520  pntlemp  23523  pntleml  23524  abvcxp  23528  ostth2lem2  23547  axtgcont1  23593  cgr3simp3  23641  legso  23712  colline  23743  wlkonwlk  24213  wwlksswrd  24364  wwlkeq  24398  clwwisshclwwn  24484  erclwwlksym  24490  erclwwlktr  24491  el2wlksoton  24554  el2spthsoton  24555  cusgraiffrusgra  24616  eupapf  24648  frrusgraord  24748  tncp  24856  grpolidinv  24879  nvs  25241  nvz  25248  nvtri  25249  sspn  25325  minvecolem2  25467  minvecolem4c  25471  minvecolem4  25472  minvecolem5  25473  minvecolem6  25474  adj1  26528  eliccelico  27256  elicoelioo  27257  slmdvsdir  27421  slmd0vs  27429  cnre2csqlem  27528  rnlogbval  27656  rnlogbcl  27657  nnlogbexp  27660  logbrec  27661  sigaclci  27772  unelsiga  27774  insiga  27777  measvun  27820  cntmeas  27837  sibfima  27920  signstfveq0  28174  tg5segofs  28193  subfacp1lem3  28266  subfacp1lem4  28267  subfacp1lem5  28268  sconpht2  28323  sconpi1  28324  txscon  28326  rescon  28331  cvmcn  28347  cvmsuni  28354  cvmsdisj  28355  cvmshmeo  28356  cvmlift2lem8  28395  cvmlift2lem13  28400  cvmliftphtlem  28402  cvmliftpht  28403  cvmlift3lem6  28409  ghomgrplem  28504  ibladdnc  29649  iblabsnclem  29655  ftc2nc  29676  dvasin  29680  ivthALT  29730  isbndx  29881  isbnd3  29883  prdsbnd  29892  heiborlem3  29912  iccbnd  29939  rngohomadd  29975  rngohommul  29976  idladdcl  30019  idllmulcl  30020  idlrmulcl  30021  maxidlmax  30043  pridlc  30071  acongrep  30522  elicore  31101  eliocre  31111  iccshift  31122  iccsuble  31123  icoiccdif  31128  mullimc  31158  limccog  31162  limciccioolb  31163  mullimcf  31165  limcperiod  31170  lptioo2  31173  lptioo1  31174  neglimc  31189  addlimc  31190  0ellimcdiv  31191  reclimc  31195  icccncfext  31226  cncfiooicclem1  31232  cncfioobdlem  31235  ditgeqiooicc  31278  iblspltprt  31291  iblcncfioo  31296  itgspltprt  31297  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  stoweidlem11  31311  stoweidlem31  31331  stoweidlem36  31336  stoweidlem38  31338  stoweidlem62  31362  dirkercncflem1  31403  dirkercncflem4  31406  fourierdlem26  31433  fourierdlem32  31439  fourierdlem33  31440  fourierdlem37  31444  fourierdlem42  31449  fourierdlem54  31461  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem74  31481  fourierdlem75  31482  fourierdlem79  31486  fourierdlem81  31488  fourierdlem82  31489  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem93  31500  fourierdlem101  31508  fourierdlem107  31514  fourierdlem109  31516  fourierdlem111  31518  sigardiv  31545  sigarcol  31548  sharhght  31549  sigaradd  31550  cevathlem1  31551  cevathlem2  31552  cevath  31553  lelttrdi  31792  bnj1018  33099  lshpnelb  33781  lshpcmp  33785  oplecon3  33996  opnoncon  34005  hlcvl  34156  dochshpncl  36181  lclkrslem1  36334  lclkrslem2  36335
  Copyright terms: Public domain W3C validator