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

Theorem simp3d 1019
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 1007 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 17 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simp3bi  1022  f1dom3fv3dif  6120  f1dom3el3dif  6121  oeeui  7251  erinxp  7385  resixp  7505  domssex2  7678  cantnflem1c  8137  cantnflem1  8139  cantnflem3  8141  cantnflem4  8142  fpwwe2lem7  9005  canthnumlem  9017  canthp1lem2  9022  wununi  9075  wunpw  9076  wunpr  9078  ixxdisj  11594  ixxun  11595  ixxss1  11597  ixxss2  11598  ixxss12  11599  ixxub  11600  ixxlb  11601  ixxlbOLD  11602  lbioo  11611  elicore  11631  iccsupr  11671  icodisj  11701  xov1plusxeqvd  11722  intfracq  12029  fldiv  12030  seqf1olem2  12196  cjmul  13142  icco1  13540  sumtp  13746  rpnnen2lem10  14212  ruclem2  14220  ruclem3  14221  ruclem9  14226  ruclem12  14229  dvdslegcd  14414  crt  14662  eulerthlem1  14665  eulerthlem2  14666  pcpremul  14729  prmreclem2  14797  prmreclem3  14798  4sqlem13OLD  14837  4sqlem13  14843  sectcan  15596  sectco  15597  sectmon  15623  monsect  15624  funcid  15711  funcco  15712  funcsect  15713  invfuc  15815  fuciso  15816  coapm  15902  catciso  15938  postr  16135  ipodrsima  16347  psref2  16386  psasym  16392  mhm0  16526  submcl  16536  submmnd  16537  eqger  16803  eqgcpbl  16807  gaorber  16898  orbsta  16903  cayleyth  16992  pmtrrn2  17037  pmtrfinv  17038  pmtrfmvdn0  17039  dfod2  17151  sylow2blem1  17208  sylow2blem3  17210  dprdcntz  17576  dprddisj  17577  dprdffsupp  17583  dpjdisj  17622  ablfac1a  17638  ablfac1b  17639  lmodvsdir  18051  lmhmlin  18194  lbsind  18239  2idlcpbl  18394  assasca  18481  mpfind  18695  mpt2frlmd  19270  mdetunilem2  19573  mdetunilem5  19576  mdetunilem6  19577  mnfnei  20172  cnprcl  20196  lmcvg  20213  lmff  20252  lmcls  20253  lmcnp  20255  fbasssin  20786  flimfil  20919  tgpconcomp  21062  tlmtrg  21139  ustssel  21155  ustincl  21157  ustdiag  21158  ustinvel  21159  ustexhalf  21160  ustfilxp  21162  tustopn  21221  tususp  21222  imasdsf1olem  21323  xmeter  21383  xmetresbl  21387  tmstopn  21435  metustexhalf  21506  nlmnrg  21617  qdensere  21725  blcvx  21751  tgqioo  21753  icccmplem1  21775  icccmplem2  21776  reconnlem1  21779  cnmpt2pc  21891  iccpnfcnv  21907  phtpcer  21961  phtpcco2  21965  pcohtpy  21986  pcorev2  21994  pcophtb  21995  om1addcl  21999  pi1blem  22005  pi1cpbl  22010  pi1grplem  22015  pi1inv  22018  pi1xfrf  22019  pi1xfr  22021  pi1xfrcnvlem  22022  pi1cof  22025  pi1coghm  22027  cphreccllem  22091  cphsca  22092  cphsubrg  22093  cphsqrtcl2  22099  tchclm  22141  tchcph  22146  lmmcvg  22166  cmetcaulem  22193  lmcau  22217  bcthlem3  22229  bcthlem4  22230  minveclem4c  22302  minveclem2  22303  minveclem3b  22305  minveclem4  22309  minveclem6  22311  minveclem4cOLD  22314  minveclem2OLD  22315  minveclem3bOLD  22317  minveclem4OLD  22321  minveclem6OLD  22323  ivthicc  22344  ovollb2lem  22376  ovolshftlem1  22397  ovolscalem1  22401  ovolicc1  22404  ovolicc2lem2  22406  ovolicc2lem3  22407  ovolicc2lem4OLD  22408  ovolicc2lem4  22409  ovolicc2lem5  22410  ioombl1lem1  22446  dyadmaxlem  22490  volivth  22500  vitalilem2  22502  vitalilem4  22504  i1fima2  22572  itg2monolem1  22643  itgcnlem  22682  itgrevallem1  22687  itgreval  22689  itgle  22702  ibladd  22713  iblabslem  22720  itgspliticc  22729  itgsplitioo  22730  ditgcl  22748  ditgswap  22749  ditgsplitlem  22750  limcdif  22766  limcresi  22775  limcres  22776  limccnp  22781  limccnp2  22782  limcun  22785  dvlip  22880  dvlip2  22882  dveq0  22887  dvgt0lem1  22889  dvivthlem1  22895  dvcnvrelem1  22904  dvcnvre  22906  dvfsumlem2  22914  ftc1lem1  22922  ftc1lem2  22923  ftc1a  22924  ftc1lem4  22926  ftc2  22931  ftc2ditglem  22932  itgsubstlem  22935  ply1rem  23049  fta1glem2  23052  ig1pdvds  23063  ig1pdvdsOLD  23069  plyrem  23193  fta1lem  23195  vieta1lem2  23199  aaliou3lem3  23235  pserulm  23312  psercnlem2  23314  psercnlem1  23315  psercn  23316  pserdvlem1  23317  pserdvlem2  23318  abelth2  23332  coseq00topi  23392  coseq0negpitopi  23393  cosordlem  23415  tanord1  23421  efif1olem1  23426  dvloglem  23528  efopnlem1  23536  logreclem  23634  relogbval  23644  nnlogbexp  23653  logbrec  23654  chordthmlem4  23696  quart1  23717  quartlem2  23719  quartlem3  23720  quart  23722  acosbnd  23761  atancj  23771  atanlogsublem  23776  atantan  23784  atanbndlem  23786  atans2  23792  dvatan  23796  atantayl  23798  divsqrtsumlem  23840  ftalem5  23936  ftalem5OLD  23938  basellem5  23946  ppisval  23965  chtleppi  24073  chpchtsum  24082  chpub  24083  mersenne  24090  perfectlem2  24093  dchrinv  24124  rplogsumlem2  24258  chpdifbndlem1  24326  pntibndlem2  24364  pntlema  24369  pntlemb  24370  pntlemg  24371  pntlemh  24372  pntlemr  24375  pntlemj  24376  pntlemf  24378  pntlemk  24379  pntlemo  24380  pntlemp  24383  pntleml  24384  abvcxp  24388  ostth2lem2  24407  axtgcont1  24451  cgr3simp3  24502  legso  24579  hlln  24587  hltr  24590  btwnhl  24594  mirhl  24659  mirbtwnhl  24660  opphllem4  24727  opphl  24731  hlpasch  24733  cgracgr  24795  cgraswap  24797  cgrahl  24803  cgracol  24804  inagswap  24815  wlkonwlk  25200  wwlksswrd  25351  wwlkeq  25385  clwwisshclwwn  25471  erclwwlksym  25477  erclwwlktr  25478  el2wlksoton  25541  el2spthsoton  25542  cusgraiffrusgra  25603  eupapf  25635  frrusgraord  25734  tncp  25845  grpolidinv  25864  nvs  26226  nvz  26233  nvtri  26234  sspn  26310  minvecolem2  26452  minvecolem4c  26456  minvecolem4  26457  minvecolem5  26458  minvecolem6  26459  minvecolem2OLD  26462  minvecolem4cOLD  26466  minvecolem4OLD  26467  minvecolem5OLD  26468  minvecolem6OLD  26469  adj1  27521  eliccelico  28302  elicoelioo  28303  slmdvsdir  28476  slmd0vs  28484  pmtrto1cl  28557  locfinreflem  28612  cnre2csqlem  28661  sigaclci  28899  unelsiga  28901  insiga  28904  unelldsys  28925  ldsysgenld  28927  sigapildsys  28929  ldgenpisyslem1  28930  measvun  28976  cntmeas  28993  sibfima  29116  signstfveq0  29411  tg5segofs  29435  bnj1018  29718  subfacp1lem3  29850  subfacp1lem4  29851  subfacp1lem5  29852  sconpht2  29906  sconpi1  29907  txscon  29909  rescon  29914  cvmcn  29930  cvmsuni  29937  cvmsdisj  29938  cvmshmeo  29939  cvmlift2lem8  29978  cvmlift2lem13  29983  cvmliftphtlem  29985  cvmliftpht  29986  cvmlift3lem6  29992  msrf  30125  elmsta  30131  mthmpps  30165  mclsppslem  30166  ghomgrplem  30252  ivthALT  30933  relowlssretop  31667  ibladdnc  31900  iblabsnclem  31906  ftc2nc  31927  dvasin  31929  isbndx  32015  isbnd3  32017  prdsbnd  32026  heiborlem3  32046  iccbnd  32073  rngohomadd  32109  rngohommul  32110  idladdcl  32153  idllmulcl  32154  idlrmulcl  32155  maxidlmax  32177  pridlc  32205  lshpnelb  32456  lshpcmp  32460  oplecon3  32671  opnoncon  32680  hlcvl  32831  dochshpncl  34858  lclkrslem1  35011  lclkrslem2  35012  acongrep  35737  cvgdvgrat  36569  binomcxplemdvbinom  36609  eliocre  37495  iccshift  37505  iccsuble  37506  icoiccdif  37511  mullimc  37573  limccog  37577  limciccioolb  37578  mullimcf  37580  limcperiod  37585  lptioo2  37588  lptioo1  37589  neglimc  37605  addlimc  37606  0ellimcdiv  37607  reclimc  37611  icccncfext  37642  cncfioobdlem  37651  ditgeqiooicc  37714  iblspltprt  37727  iblcncfioo  37732  itgiccshift  37734  itgperiod  37735  itgsbtaddcnst  37736  stoweidlem11  37748  stoweidlem31  37769  stoweidlem36  37774  stoweidlem38  37776  stoweidlem62  37800  stoweidlem62OLD  37801  dirkercncflem1  37842  dirkercncflem4  37845  fourierdlem26  37872  fourierdlem32  37879  fourierdlem33  37880  fourierdlem37  37884  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem54  37901  fourierdlem63  37910  fourierdlem64  37911  fourierdlem65  37912  fourierdlem74  37921  fourierdlem75  37922  fourierdlem79  37926  fourierdlem81  37928  fourierdlem82  37929  fourierdlem89  37936  fourierdlem90  37937  fourierdlem91  37938  fourierdlem93  37940  fourierdlem101  37948  fourierdlem107  37954  fourierdlem109  37956  fourierdlem111  37958  salunicl  38035  saluncl  38036  hoidmv1lelem1  38254  hoidmv1lelem3  38256  hoidmvlelem1  38258  sigardiv  38278  sigarcol  38281  sharhght  38282  sigaradd  38283  cevathlem1  38284  cevathlem2  38285  cevath  38286  perfectALTVlem2  38651  proththd  38721  lelttrdi  38838  umgredgne  38987  usgrnloopv  39029
  Copyright terms: Public domain W3C validator