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

Theorem simp3d 1009
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 997 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 972
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 974
This theorem is referenced by:  simp3bi  1012  f1dom3fv3dif  6156  f1dom3el3dif  6157  oeeui  7249  erinxp  7383  resixp  7502  domssex2  7675  cantnflem1c  8104  cantnflem1  8106  cantnflem3  8108  cantnflem4  8109  cantnflem1cOLD  8127  cantnflem1OLD  8129  cantnflem3OLD  8130  cantnflem4OLD  8131  fpwwe2lem7  9012  canthnumlem  9024  canthp1lem2  9029  wununi  9082  wunpw  9083  wunpr  9085  ixxdisj  11548  ixxun  11549  ixxss1  11551  ixxss2  11552  ixxss12  11553  ixxub  11554  ixxlb  11555  lbioo  11564  iccsupr  11621  icodisj  11649  xov1plusxeqvd  11670  intfracq  11960  fldiv  11961  seqf1olem2  12121  cjmul  12949  icco1  13337  rpnnen2lem10  13829  ruclem2  13837  ruclem3  13838  ruclem9  13843  ruclem12  13846  dvdslegcd  14026  crt  14180  eulerthlem1  14183  eulerthlem2  14184  pcpremul  14239  prmreclem2  14307  prmreclem3  14308  4sqlem13  14347  sectcan  15022  sectco  15023  sectmon  15044  monsect  15045  funcid  15108  funcco  15109  funcsect  15110  invfuc  15212  fuciso  15213  coapm  15267  catciso  15303  postr  15452  ipodrsima  15664  psref2  15703  psasym  15709  mhm0  15843  submcl  15853  submmnd  15854  eqger  16120  eqgcpbl  16124  gaorber  16215  orbsta  16220  cayleyth  16309  pmtrrn2  16354  pmtrfinv  16355  pmtrfmvdn0  16356  dfod2  16455  sylow2blem1  16509  sylow2blem3  16511  dprdcntz  16910  dprddisj  16911  dprdffsupp  16916  dprdffiOLD  16922  dpjdisj  16970  ablfac1a  16988  ablfac1b  16989  lmodvsdir  17404  lmhmlin  17549  lbsind  17594  2idlcpbl  17750  assasca  17838  mpfind  18073  mpt2frlmd  18675  mdetunilem2  18982  mdetunilem5  18985  mdetunilem6  18986  mnfnei  19588  cnprcl  19612  lmcvg  19629  lmff  19668  lmcls  19669  lmcnp  19671  fbasssin  20203  flimfil  20336  tgpconcomp  20477  tlmtrg  20558  ustssel  20574  ustincl  20576  ustdiag  20577  ustinvel  20578  ustexhalf  20579  ustfilxp  20581  tustopn  20640  tususp  20641  imasdsf1olem  20742  xmeter  20802  xmetresbl  20806  tmstopn  20854  metustexhalfOLD  20932  metustexhalf  20933  nlmnrg  21054  qdensere  21143  blcvx  21169  tgqioo  21171  icccmplem1  21193  icccmplem2  21194  reconnlem1  21197  cnmpt2pc  21294  iccpnfcnv  21310  phtpcer  21361  phtpcco2  21365  pcohtpy  21386  pcorev2  21394  pcophtb  21395  om1addcl  21399  pi1blem  21405  pi1cpbl  21410  pi1grplem  21415  pi1inv  21418  pi1xfrf  21419  pi1xfr  21421  pi1xfrcnvlem  21422  pi1cof  21425  pi1coghm  21427  cphreccllem  21491  cphsca  21492  cphsubrg  21493  cphsqrtcl2  21499  tchclm  21541  tchcph  21546  lmmcvg  21566  cmetcaulem  21593  lmcau  21617  bcthlem3  21631  bcthlem4  21632  minveclem4c  21706  minveclem2  21707  minveclem3b  21709  minveclem4  21713  minveclem6  21715  ivthicc  21736  ovollb2lem  21765  ovolshftlem1  21786  ovolscalem1  21790  ovolicc1  21793  ovolicc2lem2  21795  ovolicc2lem3  21796  ovolicc2lem4  21797  ovolicc2lem5  21798  ioombl1lem1  21834  dyadmaxlem  21872  volivth  21882  vitalilem2  21884  vitalilem4  21886  i1fima2  21952  itg2monolem1  22023  itgcnlem  22062  itgrevallem1  22067  itgreval  22069  itgle  22082  ibladd  22093  iblabslem  22100  itgspliticc  22109  itgsplitioo  22110  ditgcl  22128  ditgswap  22129  ditgsplitlem  22130  limcdif  22146  limcresi  22155  limcres  22156  limccnp  22161  limccnp2  22162  limcun  22165  dvlip  22260  dvlip2  22262  dveq0  22267  dvgt0lem1  22269  dvivthlem1  22275  dvcnvrelem1  22284  dvcnvre  22286  dvfsumlem2  22294  ftc1lem1  22302  ftc1lem2  22303  ftc1a  22304  ftc1lem4  22306  ftc2  22311  ftc2ditglem  22312  itgsubstlem  22315  ply1rem  22430  fta1glem2  22433  ig1pdvds  22443  plyrem  22566  fta1lem  22568  vieta1lem2  22572  aaliou3lem3  22605  pserulm  22682  psercnlem2  22684  psercnlem1  22685  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  abelth2  22702  coseq00topi  22760  coseq0negpitopi  22761  cosordlem  22783  tanord1  22789  efif1olem1  22794  dvloglem  22894  efopnlem1  22902  logreclem  23015  chordthmlem4  23031  quart1  23052  quartlem2  23054  quartlem3  23055  quart  23057  acosbnd  23096  atancj  23106  atanlogsublem  23111  atantan  23119  atanbndlem  23121  atans2  23127  dvatan  23131  atantayl  23133  divsqrtsumlem  23174  ftalem5  23215  basellem5  23223  ppisval  23242  chtleppi  23350  chpchtsum  23359  chpub  23360  mersenne  23367  perfectlem2  23370  dchrinv  23401  rplogsumlem2  23535  chpdifbndlem1  23603  pntibndlem2  23641  pntlema  23646  pntlemb  23647  pntlemg  23648  pntlemh  23649  pntlemr  23652  pntlemj  23653  pntlemf  23655  pntlemk  23656  pntlemo  23657  pntlemp  23660  pntleml  23661  abvcxp  23665  ostth2lem2  23684  axtgcont1  23730  cgr3simp3  23778  legso  23850  hlln  23856  hltr  23859  btwnhl  23863  mirhl  23924  mirbtwnhl  23925  opphllem4  23987  opphl  23990  wlkonwlk  24402  wwlksswrd  24553  wwlkeq  24587  clwwisshclwwn  24673  erclwwlksym  24679  erclwwlktr  24680  el2wlksoton  24743  el2spthsoton  24744  cusgraiffrusgra  24805  eupapf  24837  frrusgraord  24936  tncp  25045  grpolidinv  25068  nvs  25430  nvz  25437  nvtri  25438  sspn  25514  minvecolem2  25656  minvecolem4c  25660  minvecolem4  25661  minvecolem5  25662  minvecolem6  25663  adj1  26717  eliccelico  27453  elicoelioo  27454  slmdvsdir  27625  slmd0vs  27633  locfinreflem  27709  cnre2csqlem  27758  rnlogbval  27882  rnlogbcl  27883  nnlogbexp  27886  logbrec  27887  sigaclci  27998  unelsiga  28000  insiga  28003  measvun  28046  cntmeas  28063  sibfima  28146  signstfveq0  28400  tg5segofs  28419  subfacp1lem3  28492  subfacp1lem4  28493  subfacp1lem5  28494  sconpht2  28549  sconpi1  28550  txscon  28552  rescon  28557  cvmcn  28573  cvmsuni  28580  cvmsdisj  28581  cvmshmeo  28582  cvmlift2lem8  28621  cvmlift2lem13  28626  cvmliftphtlem  28628  cvmliftpht  28629  cvmlift3lem6  28635  msrf  28768  elmsta  28774  mthmpps  28808  mclsppslem  28809  ghomgrplem  28895  ibladdnc  30040  iblabsnclem  30046  ftc2nc  30067  dvasin  30071  ivthALT  30121  isbndx  30246  isbnd3  30248  prdsbnd  30257  heiborlem3  30277  iccbnd  30304  rngohomadd  30340  rngohommul  30341  idladdcl  30384  idllmulcl  30385  idlrmulcl  30386  maxidlmax  30408  pridlc  30436  acongrep  30886  cvgdvgrat  31163  elicore  31469  eliocre  31479  iccshift  31490  iccsuble  31491  icoiccdif  31496  mullimc  31526  limccog  31530  limciccioolb  31531  mullimcf  31533  limcperiod  31538  lptioo2  31541  lptioo1  31542  neglimc  31557  addlimc  31558  0ellimcdiv  31559  reclimc  31563  icccncfext  31593  cncfioobdlem  31602  ditgeqiooicc  31645  iblspltprt  31658  iblcncfioo  31663  itgiccshift  31665  itgperiod  31666  itgsbtaddcnst  31667  stoweidlem11  31678  stoweidlem31  31698  stoweidlem36  31703  stoweidlem38  31705  stoweidlem62  31729  dirkercncflem1  31770  dirkercncflem4  31773  fourierdlem26  31800  fourierdlem32  31806  fourierdlem33  31807  fourierdlem37  31811  fourierdlem42  31816  fourierdlem54  31828  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem74  31848  fourierdlem75  31849  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem93  31867  fourierdlem101  31875  fourierdlem107  31881  fourierdlem109  31883  fourierdlem111  31885  sigardiv  31912  sigarcol  31915  sharhght  31916  sigaradd  31917  cevathlem1  31918  cevathlem2  31919  cevath  31920  lelttrdi  32157  bnj1018  33727  lshpnelb  34411  lshpcmp  34415  oplecon3  34626  opnoncon  34635  hlcvl  34786  dochshpncl  36813  lclkrslem1  36966  lclkrslem2  36967
  Copyright terms: Public domain W3C validator