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

Theorem simp3d 1028
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 1016 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 17 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simp3bi  1031  f1dom3fv3dif  6193  f1dom3el3dif  6194  oeeui  7329  erinxp  7463  resixp  7583  domssex2  7758  cantnflem1c  8218  cantnflem1  8220  cantnflem3  8222  cantnflem4  8223  fpwwe2lem7  9087  canthnumlem  9099  canthp1lem2  9104  wununi  9157  wunpw  9158  wunpr  9160  ixxdisj  11679  ixxun  11680  ixxss1  11682  ixxss2  11683  ixxss12  11684  ixxub  11685  ixxlb  11686  ixxlbOLD  11687  lbioo  11696  elicore  11716  iccsupr  11756  icodisj  11786  xov1plusxeqvd  11807  intfracq  12118  fldiv  12119  seqf1olem2  12285  cjmul  13254  icco1  13653  sumtp  13859  rpnnen2lem10  14325  ruclem2  14333  ruclem3  14334  ruclem9  14339  ruclem12  14342  dvdslegcd  14527  crt  14775  eulerthlem1  14778  eulerthlem2  14779  pcpremul  14842  prmreclem2  14910  prmreclem3  14911  4sqlem13OLD  14950  4sqlem13  14956  sectcan  15709  sectco  15710  sectmon  15736  monsect  15737  funcid  15824  funcco  15825  funcsect  15826  invfuc  15928  fuciso  15929  coapm  16015  catciso  16051  postr  16248  ipodrsima  16460  psref2  16499  psasym  16505  mhm0  16639  submcl  16649  submmnd  16650  eqger  16916  eqgcpbl  16920  gaorber  17011  orbsta  17016  cayleyth  17105  pmtrrn2  17150  pmtrfinv  17151  pmtrfmvdn0  17152  dfod2  17264  sylow2blem1  17321  sylow2blem3  17323  dprdcntz  17689  dprddisj  17690  dprdffsupp  17696  dpjdisj  17735  ablfac1a  17751  ablfac1b  17752  lmodvsdir  18164  lmhmlin  18307  lbsind  18352  2idlcpbl  18507  assasca  18594  mpfind  18808  mpt2frlmd  19384  mdetunilem2  19687  mdetunilem5  19690  mdetunilem6  19691  mnfnei  20286  cnprcl  20310  lmcvg  20327  lmff  20366  lmcls  20367  lmcnp  20369  fbasssin  20900  flimfil  21033  tgpconcomp  21176  tlmtrg  21253  ustssel  21269  ustincl  21271  ustdiag  21272  ustinvel  21273  ustexhalf  21274  ustfilxp  21276  tustopn  21335  tususp  21336  imasdsf1olem  21437  xmeter  21497  xmetresbl  21501  tmstopn  21549  metustexhalf  21620  nlmnrg  21731  qdensere  21839  blcvx  21865  tgqioo  21867  icccmplem1  21889  icccmplem2  21890  reconnlem1  21893  cnmpt2pc  22005  iccpnfcnv  22021  phtpcer  22075  phtpcco2  22079  pcohtpy  22100  pcorev2  22108  pcophtb  22109  om1addcl  22113  pi1blem  22119  pi1cpbl  22124  pi1grplem  22129  pi1inv  22132  pi1xfrf  22133  pi1xfr  22135  pi1xfrcnvlem  22136  pi1cof  22139  pi1coghm  22141  cphreccllem  22205  cphsca  22206  cphsubrg  22207  cphsqrtcl2  22213  tchclm  22255  tchcph  22260  lmmcvg  22280  cmetcaulem  22307  lmcau  22331  bcthlem3  22343  bcthlem4  22344  minveclem4c  22416  minveclem2  22417  minveclem3b  22419  minveclem4  22423  minveclem6  22425  minveclem4cOLD  22428  minveclem2OLD  22429  minveclem3bOLD  22431  minveclem4OLD  22435  minveclem6OLD  22437  ivthicc  22458  ovollb2lem  22490  ovolshftlem1  22511  ovolscalem1  22515  ovolicc1  22518  ovolicc2lem2  22520  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2lem5  22524  ioombl1lem1  22560  dyadmaxlem  22604  volivth  22614  vitalilem2  22616  vitalilem4  22618  i1fima2  22686  itg2monolem1  22757  itgcnlem  22796  itgrevallem1  22801  itgreval  22803  itgle  22816  ibladd  22827  iblabslem  22834  itgspliticc  22843  itgsplitioo  22844  ditgcl  22862  ditgswap  22863  ditgsplitlem  22864  limcdif  22880  limcresi  22889  limcres  22890  limccnp  22895  limccnp2  22896  limcun  22899  dvlip  22994  dvlip2  22996  dveq0  23001  dvgt0lem1  23003  dvivthlem1  23009  dvcnvrelem1  23018  dvcnvre  23020  dvfsumlem2  23028  ftc1lem1  23036  ftc1lem2  23037  ftc1a  23038  ftc1lem4  23040  ftc2  23045  ftc2ditglem  23046  itgsubstlem  23049  ply1rem  23163  fta1glem2  23166  ig1pdvds  23177  ig1pdvdsOLD  23183  plyrem  23307  fta1lem  23309  vieta1lem2  23313  aaliou3lem3  23349  pserulm  23426  psercnlem2  23428  psercnlem1  23429  psercn  23430  pserdvlem1  23431  pserdvlem2  23432  abelth2  23446  coseq00topi  23506  coseq0negpitopi  23507  cosordlem  23529  tanord1  23535  efif1olem1  23540  dvloglem  23642  efopnlem1  23650  logreclem  23748  relogbval  23758  nnlogbexp  23767  logbrec  23768  chordthmlem4  23810  quart1  23831  quartlem2  23833  quartlem3  23834  quart  23836  acosbnd  23875  atancj  23885  atanlogsublem  23890  atantan  23898  atanbndlem  23900  atans2  23906  dvatan  23910  atantayl  23912  divsqrtsumlem  23954  ftalem5  24050  ftalem5OLD  24052  basellem5  24060  ppisval  24079  chtleppi  24187  chpchtsum  24196  chpub  24197  mersenne  24204  perfectlem2  24207  dchrinv  24238  rplogsumlem2  24372  chpdifbndlem1  24440  pntibndlem2  24478  pntlema  24483  pntlemb  24484  pntlemg  24485  pntlemh  24486  pntlemr  24489  pntlemj  24490  pntlemf  24492  pntlemk  24493  pntlemo  24494  pntlemp  24497  pntleml  24498  abvcxp  24502  ostth2lem2  24521  axtgcont1  24565  cgr3simp3  24616  legso  24693  hlln  24701  hltr  24704  btwnhl  24708  mirhl  24773  mirbtwnhl  24774  opphllem4  24841  opphl  24845  hlpasch  24847  cgracgr  24909  cgraswap  24911  cgrahl  24917  cgracol  24918  inagswap  24929  wlkonwlk  25314  wwlksswrd  25465  wwlkeq  25499  clwwisshclwwn  25585  erclwwlksym  25591  erclwwlktr  25592  el2wlksoton  25655  el2spthsoton  25656  cusgraiffrusgra  25717  eupapf  25749  frrusgraord  25848  tncp  25959  grpolidinv  25978  nvs  26340  nvz  26347  nvtri  26348  sspn  26424  minvecolem2  26566  minvecolem4c  26570  minvecolem4  26571  minvecolem5  26572  minvecolem6  26573  minvecolem2OLD  26576  minvecolem4cOLD  26580  minvecolem4OLD  26581  minvecolem5OLD  26582  minvecolem6OLD  26583  adj1  27635  eliccelico  28408  elicoelioo  28409  slmdvsdir  28581  slmd0vs  28589  pmtrto1cl  28661  locfinreflem  28716  cnre2csqlem  28765  sigaclci  29003  unelsiga  29005  insiga  29008  unelldsys  29029  ldsysgenld  29031  sigapildsys  29033  ldgenpisyslem1  29034  measvun  29080  cntmeas  29097  sibfima  29220  signstfveq0  29515  tg5segofs  29539  bnj1018  29822  subfacp1lem3  29954  subfacp1lem4  29955  subfacp1lem5  29956  sconpht2  30010  sconpi1  30011  txscon  30013  rescon  30018  cvmcn  30034  cvmsuni  30041  cvmsdisj  30042  cvmshmeo  30043  cvmlift2lem8  30082  cvmlift2lem13  30087  cvmliftphtlem  30089  cvmliftpht  30090  cvmlift3lem6  30096  msrf  30229  elmsta  30235  mthmpps  30269  mclsppslem  30270  ghomgrplem  30356  ivthALT  31040  relowlssretop  31811  ibladdnc  32044  iblabsnclem  32050  ftc2nc  32071  dvasin  32073  isbndx  32159  isbnd3  32161  prdsbnd  32170  heiborlem3  32190  iccbnd  32217  rngohomadd  32253  rngohommul  32254  idladdcl  32297  idllmulcl  32298  idlrmulcl  32299  maxidlmax  32321  pridlc  32349  lshpnelb  32595  lshpcmp  32599  oplecon3  32810  opnoncon  32819  hlcvl  32970  dochshpncl  34997  lclkrslem1  35150  lclkrslem2  35151  acongrep  35875  cvgdvgrat  36706  binomcxplemdvbinom  36746  fvixp2  37516  eliocre  37647  iccshift  37657  iccsuble  37658  icoiccdif  37663  mullimc  37734  limccog  37738  limciccioolb  37739  mullimcf  37741  limcperiod  37746  lptioo2  37749  lptioo1  37750  neglimc  37766  addlimc  37767  0ellimcdiv  37768  reclimc  37772  icccncfext  37803  cncfioobdlem  37812  ditgeqiooicc  37875  iblspltprt  37888  iblcncfioo  37893  itgiccshift  37895  itgperiod  37896  itgsbtaddcnst  37897  stoweidlem11  37909  stoweidlem31  37930  stoweidlem36  37935  stoweidlem38  37937  stoweidlem62  37961  stoweidlem62OLD  37962  dirkercncflem1  38003  dirkercncflem4  38006  fourierdlem26  38033  fourierdlem32  38040  fourierdlem33  38041  fourierdlem37  38045  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem54  38062  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem74  38082  fourierdlem75  38083  fourierdlem79  38087  fourierdlem81  38089  fourierdlem82  38090  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem93  38101  fourierdlem101  38109  fourierdlem107  38115  fourierdlem109  38117  fourierdlem111  38119  salunicl  38215  saluncl  38216  hoidmv1lelem1  38451  hoidmv1lelem3  38453  hoidmvlelem1  38455  sigardiv  38508  sigarcol  38511  sharhght  38512  sigaradd  38513  cevathlem1  38514  cevathlem2  38515  cevath  38516  perfectALTVlem2  38882  proththd  38952  lelttrdi  39089  umgrnloopv  39242  umgredgne  39281  usgrnloopvALT  39332  cusgrm1rusgr  39648  21wlkdlem6  39880  21wlkond  39886  2trlond  39888
  Copyright terms: Public domain W3C validator