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

Theorem simp3d 1008
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 996 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simp3bi  1011  f1dom3fv3dif  6150  f1dom3el3dif  6151  oeeui  7243  erinxp  7377  resixp  7497  domssex2  7670  cantnflem1c  8097  cantnflem1  8099  cantnflem3  8101  cantnflem4  8102  cantnflem1cOLD  8120  cantnflem1OLD  8122  cantnflem3OLD  8123  cantnflem4OLD  8124  fpwwe2lem7  9003  canthnumlem  9015  canthp1lem2  9020  wununi  9073  wunpw  9074  wunpr  9076  ixxdisj  11547  ixxun  11548  ixxss1  11550  ixxss2  11551  ixxss12  11552  ixxub  11553  ixxlb  11554  lbioo  11563  iccsupr  11620  icodisj  11648  xov1plusxeqvd  11669  intfracq  11968  fldiv  11969  seqf1olem2  12132  cjmul  13060  icco1  13448  rpnnen2lem10  14044  ruclem2  14052  ruclem3  14053  ruclem9  14058  ruclem12  14061  dvdslegcd  14241  crt  14395  eulerthlem1  14398  eulerthlem2  14399  pcpremul  14454  prmreclem2  14522  prmreclem3  14523  4sqlem13  14562  sectcan  15246  sectco  15247  sectmon  15273  monsect  15274  funcid  15361  funcco  15362  funcsect  15363  invfuc  15465  fuciso  15466  coapm  15552  catciso  15588  postr  15785  ipodrsima  15997  psref2  16036  psasym  16042  mhm0  16176  submcl  16186  submmnd  16187  eqger  16453  eqgcpbl  16457  gaorber  16548  orbsta  16553  cayleyth  16642  pmtrrn2  16687  pmtrfinv  16688  pmtrfmvdn0  16689  dfod2  16788  sylow2blem1  16842  sylow2blem3  16844  dprdcntz  17239  dprddisj  17240  dprdffsupp  17246  dprdffiOLD  17252  dpjdisj  17300  ablfac1a  17318  ablfac1b  17319  lmodvsdir  17734  lmhmlin  17879  lbsind  17924  2idlcpbl  18080  assasca  18168  mpfind  18403  mpt2frlmd  18982  mdetunilem2  19285  mdetunilem5  19288  mdetunilem6  19289  mnfnei  19892  cnprcl  19916  lmcvg  19933  lmff  19972  lmcls  19973  lmcnp  19975  fbasssin  20506  flimfil  20639  tgpconcomp  20780  tlmtrg  20861  ustssel  20877  ustincl  20879  ustdiag  20880  ustinvel  20881  ustexhalf  20882  ustfilxp  20884  tustopn  20943  tususp  20944  imasdsf1olem  21045  xmeter  21105  xmetresbl  21109  tmstopn  21157  metustexhalfOLD  21235  metustexhalf  21236  nlmnrg  21357  qdensere  21446  blcvx  21472  tgqioo  21474  icccmplem1  21496  icccmplem2  21497  reconnlem1  21500  cnmpt2pc  21597  iccpnfcnv  21613  phtpcer  21664  phtpcco2  21668  pcohtpy  21689  pcorev2  21697  pcophtb  21698  om1addcl  21702  pi1blem  21708  pi1cpbl  21713  pi1grplem  21718  pi1inv  21721  pi1xfrf  21722  pi1xfr  21724  pi1xfrcnvlem  21725  pi1cof  21728  pi1coghm  21730  cphreccllem  21794  cphsca  21795  cphsubrg  21796  cphsqrtcl2  21802  tchclm  21844  tchcph  21849  lmmcvg  21869  cmetcaulem  21896  lmcau  21920  bcthlem3  21934  bcthlem4  21935  minveclem4c  22009  minveclem2  22010  minveclem3b  22012  minveclem4  22016  minveclem6  22018  ivthicc  22039  ovollb2lem  22068  ovolshftlem1  22089  ovolscalem1  22093  ovolicc1  22096  ovolicc2lem2  22098  ovolicc2lem3  22099  ovolicc2lem4  22100  ovolicc2lem5  22101  ioombl1lem1  22137  dyadmaxlem  22175  volivth  22185  vitalilem2  22187  vitalilem4  22189  i1fima2  22255  itg2monolem1  22326  itgcnlem  22365  itgrevallem1  22370  itgreval  22372  itgle  22385  ibladd  22396  iblabslem  22403  itgspliticc  22412  itgsplitioo  22413  ditgcl  22431  ditgswap  22432  ditgsplitlem  22433  limcdif  22449  limcresi  22458  limcres  22459  limccnp  22464  limccnp2  22465  limcun  22468  dvlip  22563  dvlip2  22565  dveq0  22570  dvgt0lem1  22572  dvivthlem1  22578  dvcnvrelem1  22587  dvcnvre  22589  dvfsumlem2  22597  ftc1lem1  22605  ftc1lem2  22606  ftc1a  22607  ftc1lem4  22609  ftc2  22614  ftc2ditglem  22615  itgsubstlem  22618  ply1rem  22733  fta1glem2  22736  ig1pdvds  22746  plyrem  22870  fta1lem  22872  vieta1lem2  22876  aaliou3lem3  22909  pserulm  22986  psercnlem2  22988  psercnlem1  22989  psercn  22990  pserdvlem1  22991  pserdvlem2  22992  abelth2  23006  coseq00topi  23064  coseq0negpitopi  23065  cosordlem  23087  tanord1  23093  efif1olem1  23098  dvloglem  23200  efopnlem1  23208  logreclem  23304  relogbval  23314  nnlogbexp  23323  logbrec  23324  chordthmlem4  23366  quart1  23387  quartlem2  23389  quartlem3  23390  quart  23392  acosbnd  23431  atancj  23441  atanlogsublem  23446  atantan  23454  atanbndlem  23456  atans2  23462  dvatan  23466  atantayl  23468  divsqrtsumlem  23510  ftalem5  23551  basellem5  23559  ppisval  23578  chtleppi  23686  chpchtsum  23695  chpub  23696  mersenne  23703  perfectlem2  23706  dchrinv  23737  rplogsumlem2  23871  chpdifbndlem1  23939  pntibndlem2  23977  pntlema  23982  pntlemb  23983  pntlemg  23984  pntlemh  23985  pntlemr  23988  pntlemj  23989  pntlemf  23991  pntlemk  23992  pntlemo  23993  pntlemp  23996  pntleml  23997  abvcxp  24001  ostth2lem2  24020  axtgcont1  24066  cgr3simp3  24117  legso  24189  hlln  24195  hltr  24198  btwnhl  24202  mirhl  24263  mirbtwnhl  24264  opphllem4  24326  opphl  24329  wlkonwlk  24742  wwlksswrd  24893  wwlkeq  24927  clwwisshclwwn  25013  erclwwlksym  25019  erclwwlktr  25020  el2wlksoton  25083  el2spthsoton  25084  cusgraiffrusgra  25145  eupapf  25177  frrusgraord  25276  tncp  25385  grpolidinv  25404  nvs  25766  nvz  25773  nvtri  25774  sspn  25850  minvecolem2  25992  minvecolem4c  25996  minvecolem4  25997  minvecolem5  25998  minvecolem6  25999  adj1  27053  eliccelico  27825  elicoelioo  27826  slmdvsdir  27996  slmd0vs  28004  locfinreflem  28081  cnre2csqlem  28130  sigaclci  28365  unelsiga  28367  insiga  28370  sigapildsys  28391  measvun  28420  cntmeas  28437  sibfima  28547  signstfveq0  28801  tg5segofs  28820  subfacp1lem3  28893  subfacp1lem4  28894  subfacp1lem5  28895  sconpht2  28950  sconpi1  28951  txscon  28953  rescon  28958  cvmcn  28974  cvmsuni  28981  cvmsdisj  28982  cvmshmeo  28983  cvmlift2lem8  29022  cvmlift2lem13  29027  cvmliftphtlem  29029  cvmliftpht  29030  cvmlift3lem6  29036  msrf  29169  elmsta  29175  mthmpps  29209  mclsppslem  29210  ghomgrplem  29296  ibladdnc  30315  iblabsnclem  30321  ftc2nc  30342  dvasin  30346  ivthALT  30396  isbndx  30521  isbnd3  30523  prdsbnd  30532  heiborlem3  30552  iccbnd  30579  rngohomadd  30615  rngohommul  30616  idladdcl  30659  idllmulcl  30660  idlrmulcl  30661  maxidlmax  30683  pridlc  30711  acongrep  31160  cvgdvgrat  31438  binomcxplemdvbinom  31502  elicore  31779  eliocre  31789  iccshift  31800  iccsuble  31801  icoiccdif  31806  mullimc  31864  limccog  31868  limciccioolb  31869  mullimcf  31871  limcperiod  31876  lptioo2  31879  lptioo1  31880  neglimc  31895  addlimc  31896  0ellimcdiv  31897  reclimc  31901  icccncfext  31932  cncfioobdlem  31941  ditgeqiooicc  32001  iblspltprt  32014  iblcncfioo  32019  itgiccshift  32021  itgperiod  32022  itgsbtaddcnst  32023  stoweidlem11  32035  stoweidlem31  32055  stoweidlem36  32060  stoweidlem38  32062  stoweidlem62  32086  dirkercncflem1  32127  dirkercncflem4  32130  fourierdlem26  32157  fourierdlem32  32163  fourierdlem33  32164  fourierdlem37  32168  fourierdlem42  32173  fourierdlem54  32185  fourierdlem63  32194  fourierdlem64  32195  fourierdlem65  32196  fourierdlem74  32205  fourierdlem75  32206  fourierdlem79  32210  fourierdlem81  32212  fourierdlem82  32213  fourierdlem89  32220  fourierdlem90  32221  fourierdlem91  32222  fourierdlem93  32224  fourierdlem101  32232  fourierdlem107  32238  fourierdlem109  32240  fourierdlem111  32242  sigardiv  32320  sigarcol  32323  sharhght  32324  sigaradd  32325  cevathlem1  32326  cevathlem2  32327  cevath  32328  perfectALTVlem2  32616  proththd  32620  lelttrdi  32716  bnj1018  34440  lshpnelb  35125  lshpcmp  35129  oplecon3  35340  opnoncon  35349  hlcvl  35500  dochshpncl  37527  lclkrslem1  37680  lclkrslem2  37681
  Copyright terms: Public domain W3C validator