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

Theorem simp3d 970
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935
This theorem is referenced by:  simp3bi  973  oeeui  6742  erinxp  6875  resixp  6994  domssex2  7164  cantnflem1c  7536  cantnflem1  7538  cantnflem3  7540  cantnflem4  7541  fpwwe2lem7  8405  canthnumlem  8417  canthp1lem2  8422  wununi  8475  wunpw  8476  wunpr  8478  ixxdisj  10824  ixxun  10825  ixxss1  10827  ixxss2  10828  ixxss12  10829  ixxub  10830  ixxlb  10831  lbioo  10840  iccsupr  10889  icodisj  10914  xov1plusxeqvd  10933  intfracq  11127  fldiv  11128  seqf1olem2  11250  cjmul  11834  icco1  12221  rpnnen2lem10  12710  ruclem2  12718  ruclem3  12719  ruclem9  12724  ruclem12  12727  dvdslegcd  12903  crt  13054  eulerthlem1  13057  eulerthlem2  13058  pcpremul  13104  prmreclem2  13172  prmreclem3  13173  4sqlem13  13212  sectcan  13868  sectco  13869  sectmon  13890  monsect  13891  funcid  13954  funcco  13955  funcsect  13956  invfuc  14058  fuciso  14059  coapm  14113  catciso  14149  postr  14297  ipodrsima  14478  psref2  14523  psasym  14529  mhm0  14633  submcl  14640  submmnd  14641  eqger  14877  eqgcpbl  14881  gaorber  14972  orbsta  14977  cayleyth  15000  dfod2  15087  sylow2blem1  15141  sylow2blem3  15143  dprdcntz  15453  dprddisj  15454  dprdffi  15459  dpjdisj  15498  ablfac1a  15514  ablfac1b  15515  lmodvsdir  15862  lmhmlin  16002  lbsind  16043  2idlcpbl  16196  assasca  16272  mnfnei  17168  cnprcl  17192  lmcvg  17209  lmff  17246  lmcls  17247  lmcnp  17249  fbasssin  17744  flimfil  17877  tgpconcomp  18008  tlmtrg  18085  imasdsf1olem  18150  xmeter  18192  xmetresbl  18196  tmstopn  18244  nlmnrg  18403  qdensere  18492  blcvx  18517  tgqioo  18519  icccmplem1  18541  icccmplem2  18542  reconnlem1  18545  cnmpt2pc  18641  iccpnfcnv  18657  phtpcer  18708  phtpcco2  18712  pcohtpy  18733  pcorev2  18741  pcophtb  18742  om1addcl  18746  pi1blem  18752  pi1cpbl  18757  pi1grplem  18762  pi1inv  18765  pi1xfrf  18766  pi1xfr  18768  pi1xfrcnvlem  18769  pi1cof  18772  pi1coghm  18774  cphreccllem  18829  cphsca  18830  cphsubrg  18831  cphsqrcl2  18837  tchclm  18877  tchcph  18882  lmmcvg  18902  cmetcaulem  18929  lmcau  18953  bcthlem3  18963  bcthlem4  18964  minveclem4c  19004  minveclem2  19005  minveclem3b  19007  minveclem4  19011  minveclem6  19013  ivthicc  19033  ovollb2lem  19062  ovolshftlem1  19083  ovolscalem1  19087  ovolicc1  19090  ovolicc2lem2  19092  ovolicc2lem3  19093  ovolicc2lem4  19094  ovolicc2lem5  19095  ioombl1lem1  19130  dyadmaxlem  19167  volivth  19177  vitalilem2  19179  vitalilem4  19181  i1fima2  19249  itg2monolem1  19320  itgcnlem  19359  itgrevallem1  19364  itgreval  19366  itgle  19379  ibladd  19390  iblabslem  19397  itgspliticc  19406  itgsplitioo  19407  ditgcl  19423  ditgswap  19424  ditgsplitlem  19425  limcdif  19441  limcresi  19450  limcres  19451  limccnp  19456  limccnp2  19457  limcun  19460  dvlip  19555  dvlip2  19557  dveq0  19562  dvgt0lem1  19564  dvivthlem1  19570  dvcnvrelem1  19579  dvcnvre  19581  dvfsumlem2  19589  ftc1lem1  19597  ftc1lem2  19598  ftc1a  19599  ftc1lem4  19601  ftc2  19606  ftc2ditglem  19607  itgsubstlem  19610  mpfind  19643  ply1rem  19764  fta1glem2  19767  ig1pdvds  19777  plyrem  19900  fta1lem  19902  vieta1lem2  19906  aaliou3lem3  19939  pserulm  20016  psercnlem2  20018  psercnlem1  20019  psercn  20020  pserdvlem1  20021  pserdvlem2  20022  abelth2  20036  coseq00topi  20088  coseq0negpitopi  20089  cosordlem  20111  tanord1  20117  efif1olem1  20122  dvloglem  20217  efopnlem1  20225  logreclem  20338  chordthmlem4  20354  quart1  20374  quartlem2  20376  quartlem3  20377  quart  20379  acosbnd  20418  atancj  20428  atanlogsublem  20433  atantan  20441  atanbndlem  20443  atans2  20449  dvatan  20453  atantayl  20455  divsqrsumlem  20496  ftalem5  20537  basellem5  20545  ppisval  20564  chtleppi  20672  chpchtsum  20681  chpub  20682  mersenne  20689  perfectlem2  20692  dchrinv  20723  rplogsumlem2  20857  chpdifbndlem1  20925  pntibndlem2  20963  pntlema  20968  pntlemb  20969  pntlemg  20970  pntlemh  20971  pntlemr  20974  pntlemj  20975  pntlemf  20977  pntlemk  20978  pntlemo  20979  pntlemp  20982  pntleml  20983  abvcxp  20987  ostth2lem2  21006  eupapf  21205  tncp  21277  grpolidinv  21300  nvs  21662  nvz  21669  nvtri  21670  sspn  21746  minvecolem2  21888  minvecolem4c  21892  minvecolem4  21893  minvecolem5  21894  minvecolem6  21895  adj1  22947  eliccelico  23662  elicoelioo  23663  cnre2csqlem  23784  xrge0iifhom  23799  ustssel  23831  ustincl  23833  ustdiag  23834  ustinvel  23835  ustexhalf  23836  ustfilxp  23838  ustref  23842  tustopn  23889  tususp  23890  metustexhalf  23920  rnlogbval  23986  rnlogbcl  23987  nnlogbexp  23990  logbrec  23991  sigaclci  24101  unelsiga  24103  insiga  24106  measvun  24147  cntmeas  24164  subfacp1lem3  24437  subfacp1lem4  24438  subfacp1lem5  24439  sconpht2  24493  sconpi1  24494  txscon  24496  rescon  24501  cvmcn  24517  cvmsuni  24524  cvmsdisj  24525  cvmshmeo  24526  cvmlift2lem8  24565  cvmlift2lem13  24570  cvmliftphtlem  24572  cvmliftpht  24573  cvmlift3lem6  24579  ghomgrplem  24668  ibladdnc  25765  iblabsnclem  25771  ivthALT  25850  isbndx  26097  isbnd3  26099  prdsbnd  26108  heiborlem3  26128  iccbnd  26155  rngohomadd  26191  rngohommul  26192  idladdcl  26235  idllmulcl  26236  idlrmulcl  26237  maxidlmax  26259  pridlc  26287  acongrep  26658  pmtrfinv  26993  pmtrfmvdn0  26994  stoweidlem11  27351  stoweidlem31  27371  stoweidlem36  27376  stoweidlem62  27402  sigardiv  27442  sigarcol  27445  sharhght  27446  sigaradd  27447  cevathlem1  27448  cevathlem2  27449  cevath  27450  wlkonwlk  27698  bnj1018  28746  lshpnelb  29233  lshpcmp  29237  oplecon3  29448  opnoncon  29457  hlcvl  29608  dochshpncl  31633  lclkrslem1  31786  lclkrslem2  31787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 937
  Copyright terms: Public domain W3C validator