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  6183  f1dom3el3dif  6184  oeeui  7311  erinxp  7445  resixp  7565  domssex2  7738  cantnflem1c  8191  cantnflem1  8193  cantnflem3  8195  cantnflem4  8196  fpwwe2lem7  9060  canthnumlem  9072  canthp1lem2  9077  wununi  9130  wunpw  9131  wunpr  9133  ixxdisj  11650  ixxun  11651  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  lbioo  11667  elicore  11687  iccsupr  11727  icodisj  11755  xov1plusxeqvd  11776  intfracq  12083  fldiv  12084  seqf1olem2  12250  cjmul  13184  icco1  13582  sumtp  13788  rpnnen2lem10  14254  ruclem2  14262  ruclem3  14263  ruclem9  14268  ruclem12  14271  dvdslegcd  14452  crt  14695  eulerthlem1  14698  eulerthlem2  14699  pcpremul  14756  prmreclem2  14824  prmreclem3  14825  4sqlem13OLD  14864  4sqlem13  14870  sectcan  15611  sectco  15612  sectmon  15638  monsect  15639  funcid  15726  funcco  15727  funcsect  15728  invfuc  15830  fuciso  15831  coapm  15917  catciso  15953  postr  16150  ipodrsima  16362  psref2  16401  psasym  16407  mhm0  16541  submcl  16551  submmnd  16552  eqger  16818  eqgcpbl  16822  gaorber  16913  orbsta  16918  cayleyth  17007  pmtrrn2  17052  pmtrfinv  17053  pmtrfmvdn0  17054  dfod2  17153  sylow2blem1  17207  sylow2blem3  17209  dprdcntz  17575  dprddisj  17576  dprdffsupp  17582  dpjdisj  17621  ablfac1a  17637  ablfac1b  17638  lmodvsdir  18050  lmhmlin  18193  lbsind  18238  2idlcpbl  18393  assasca  18480  mpfind  18694  mpt2frlmd  19266  mdetunilem2  19569  mdetunilem5  19572  mdetunilem6  19573  mnfnei  20168  cnprcl  20192  lmcvg  20209  lmff  20248  lmcls  20249  lmcnp  20251  fbasssin  20782  flimfil  20915  tgpconcomp  21058  tlmtrg  21135  ustssel  21151  ustincl  21153  ustdiag  21154  ustinvel  21155  ustexhalf  21156  ustfilxp  21158  tustopn  21217  tususp  21218  imasdsf1olem  21319  xmeter  21379  xmetresbl  21383  tmstopn  21431  metustexhalf  21502  nlmnrg  21613  qdensere  21701  blcvx  21727  tgqioo  21729  icccmplem1  21751  icccmplem2  21752  reconnlem1  21755  cnmpt2pc  21852  iccpnfcnv  21868  phtpcer  21919  phtpcco2  21923  pcohtpy  21944  pcorev2  21952  pcophtb  21953  om1addcl  21957  pi1blem  21963  pi1cpbl  21968  pi1grplem  21973  pi1inv  21976  pi1xfrf  21977  pi1xfr  21979  pi1xfrcnvlem  21980  pi1cof  21983  pi1coghm  21985  cphreccllem  22049  cphsca  22050  cphsubrg  22051  cphsqrtcl2  22057  tchclm  22099  tchcph  22104  lmmcvg  22124  cmetcaulem  22151  lmcau  22175  bcthlem3  22187  bcthlem4  22188  minveclem4c  22260  minveclem2  22261  minveclem3b  22263  minveclem4  22267  minveclem6  22269  ivthicc  22290  ovollb2lem  22319  ovolshftlem1  22340  ovolscalem1  22344  ovolicc1  22347  ovolicc2lem2  22349  ovolicc2lem3  22350  ovolicc2lem4  22351  ovolicc2lem5  22352  ioombl1lem1  22388  dyadmaxlem  22432  volivth  22442  vitalilem2  22444  vitalilem4  22446  i1fima2  22514  itg2monolem1  22585  itgcnlem  22624  itgrevallem1  22629  itgreval  22631  itgle  22644  ibladd  22655  iblabslem  22662  itgspliticc  22671  itgsplitioo  22672  ditgcl  22690  ditgswap  22691  ditgsplitlem  22692  limcdif  22708  limcresi  22717  limcres  22718  limccnp  22723  limccnp2  22724  limcun  22727  dvlip  22822  dvlip2  22824  dveq0  22829  dvgt0lem1  22831  dvivthlem1  22837  dvcnvrelem1  22846  dvcnvre  22848  dvfsumlem2  22856  ftc1lem1  22864  ftc1lem2  22865  ftc1a  22866  ftc1lem4  22868  ftc2  22873  ftc2ditglem  22874  itgsubstlem  22877  ply1rem  22989  fta1glem2  22992  ig1pdvds  23002  plyrem  23126  fta1lem  23128  vieta1lem2  23132  aaliou3lem3  23165  pserulm  23242  psercnlem2  23244  psercnlem1  23245  psercn  23246  pserdvlem1  23247  pserdvlem2  23248  abelth2  23262  coseq00topi  23322  coseq0negpitopi  23323  cosordlem  23345  tanord1  23351  efif1olem1  23356  dvloglem  23458  efopnlem1  23466  logreclem  23564  relogbval  23574  nnlogbexp  23583  logbrec  23584  chordthmlem4  23626  quart1  23647  quartlem2  23649  quartlem3  23650  quart  23652  acosbnd  23691  atancj  23701  atanlogsublem  23706  atantan  23714  atanbndlem  23716  atans2  23722  dvatan  23726  atantayl  23728  divsqrtsumlem  23770  ftalem5  23866  basellem5  23874  ppisval  23893  chtleppi  24001  chpchtsum  24010  chpub  24011  mersenne  24018  perfectlem2  24021  dchrinv  24052  rplogsumlem2  24186  chpdifbndlem1  24254  pntibndlem2  24292  pntlema  24297  pntlemb  24298  pntlemg  24299  pntlemh  24300  pntlemr  24303  pntlemj  24304  pntlemf  24306  pntlemk  24307  pntlemo  24308  pntlemp  24311  pntleml  24312  abvcxp  24316  ostth2lem2  24335  axtgcont1  24379  cgr3simp3  24429  legso  24504  hlln  24512  hltr  24515  btwnhl  24519  mirhl  24583  mirbtwnhl  24584  opphllem4  24649  opphl  24653  cgracgr  24716  cgraswap  24718  cgrahl  24723  cgracol  24724  inagswap  24733  wlkonwlk  25110  wwlksswrd  25261  wwlkeq  25295  clwwisshclwwn  25381  erclwwlksym  25387  erclwwlktr  25388  el2wlksoton  25451  el2spthsoton  25452  cusgraiffrusgra  25513  eupapf  25545  frrusgraord  25644  tncp  25755  grpolidinv  25774  nvs  26136  nvz  26143  nvtri  26144  sspn  26220  minvecolem2  26362  minvecolem4c  26366  minvecolem4  26367  minvecolem5  26368  minvecolem6  26369  adj1  27421  eliccelico  28195  elicoelioo  28196  slmdvsdir  28370  slmd0vs  28378  pmtrto1cl  28451  locfinreflem  28506  cnre2csqlem  28555  sigaclci  28793  unelsiga  28795  insiga  28798  unelldsys  28819  ldsysgenld  28821  sigapildsys  28823  ldgenpisyslem1  28824  measvun  28870  cntmeas  28887  sibfima  28999  signstfveq0  29254  tg5segofs  29278  bnj1018  29561  subfacp1lem3  29693  subfacp1lem4  29694  subfacp1lem5  29695  sconpht2  29749  sconpi1  29750  txscon  29752  rescon  29757  cvmcn  29773  cvmsuni  29780  cvmsdisj  29781  cvmshmeo  29782  cvmlift2lem8  29821  cvmlift2lem13  29826  cvmliftphtlem  29828  cvmliftpht  29829  cvmlift3lem6  29835  msrf  29968  elmsta  29974  mthmpps  30008  mclsppslem  30009  ghomgrplem  30095  ivthALT  30776  relowlssretop  31500  ibladdnc  31703  iblabsnclem  31709  ftc2nc  31730  dvasin  31732  isbndx  31818  isbnd3  31820  prdsbnd  31829  heiborlem3  31849  iccbnd  31876  rngohomadd  31912  rngohommul  31913  idladdcl  31956  idllmulcl  31957  idlrmulcl  31958  maxidlmax  31980  pridlc  32008  lshpnelb  32259  lshpcmp  32263  oplecon3  32474  opnoncon  32483  hlcvl  32634  dochshpncl  34661  lclkrslem1  34814  lclkrslem2  34815  acongrep  35536  cvgdvgrat  36299  binomcxplemdvbinom  36339  eliocre  37194  iccshift  37204  iccsuble  37205  icoiccdif  37210  mullimc  37268  limccog  37272  limciccioolb  37273  mullimcf  37275  limcperiod  37280  lptioo2  37283  lptioo1  37284  neglimc  37300  addlimc  37301  0ellimcdiv  37302  reclimc  37306  icccncfext  37337  cncfioobdlem  37346  ditgeqiooicc  37406  iblspltprt  37419  iblcncfioo  37424  itgiccshift  37426  itgperiod  37427  itgsbtaddcnst  37428  stoweidlem11  37440  stoweidlem31  37461  stoweidlem36  37466  stoweidlem38  37468  stoweidlem62  37492  stoweidlem62OLD  37493  dirkercncflem1  37534  dirkercncflem4  37537  fourierdlem26  37564  fourierdlem32  37570  fourierdlem33  37571  fourierdlem37  37575  fourierdlem42  37580  fourierdlem54  37592  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem74  37612  fourierdlem75  37613  fourierdlem79  37617  fourierdlem81  37619  fourierdlem82  37620  fourierdlem89  37627  fourierdlem90  37628  fourierdlem91  37629  fourierdlem93  37631  fourierdlem101  37639  fourierdlem107  37645  fourierdlem109  37647  fourierdlem111  37649  salunicl  37724  saluncl  37725  sigardiv  37870  sigarcol  37873  sharhght  37874  sigaradd  37875  cevathlem1  37876  cevathlem2  37877  cevath  37878  perfectALTVlem2  38234  proththd  38304  lelttrdi  38396
  Copyright terms: Public domain W3C validator