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

Theorem simp3d 971
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp3bi  974  oeeui  6808  erinxp  6941  resixp  7060  domssex2  7230  cantnflem1c  7603  cantnflem1  7605  cantnflem3  7607  cantnflem4  7608  fpwwe2lem7  8471  canthnumlem  8483  canthp1lem2  8488  wununi  8541  wunpw  8542  wunpr  8544  ixxdisj  10891  ixxun  10892  ixxss1  10894  ixxss2  10895  ixxss12  10896  ixxub  10897  ixxlb  10898  lbioo  10907  iccsupr  10957  icodisj  10982  xov1plusxeqvd  11001  intfracq  11199  fldiv  11200  seqf1olem2  11322  cjmul  11906  icco1  12293  rpnnen2lem10  12782  ruclem2  12790  ruclem3  12791  ruclem9  12796  ruclem12  12799  dvdslegcd  12975  crt  13126  eulerthlem1  13129  eulerthlem2  13130  pcpremul  13176  prmreclem2  13244  prmreclem3  13245  4sqlem13  13284  sectcan  13940  sectco  13941  sectmon  13962  monsect  13963  funcid  14026  funcco  14027  funcsect  14028  invfuc  14130  fuciso  14131  coapm  14185  catciso  14221  postr  14369  ipodrsima  14550  psref2  14595  psasym  14601  mhm0  14705  submcl  14712  submmnd  14713  eqger  14949  eqgcpbl  14953  gaorber  15044  orbsta  15049  cayleyth  15072  dfod2  15159  sylow2blem1  15213  sylow2blem3  15215  dprdcntz  15525  dprddisj  15526  dprdffi  15531  dpjdisj  15570  ablfac1a  15586  ablfac1b  15587  lmodvsdir  15933  lmhmlin  16070  lbsind  16111  2idlcpbl  16264  assasca  16340  mnfnei  17243  cnprcl  17267  lmcvg  17284  lmff  17323  lmcls  17324  lmcnp  17326  fbasssin  17825  flimfil  17958  tgpconcomp  18099  tlmtrg  18176  ustssel  18192  ustincl  18194  ustdiag  18195  ustinvel  18196  ustexhalf  18197  ustfilxp  18199  tustopn  18258  tususp  18259  imasdsf1olem  18360  xmeter  18420  xmetresbl  18424  tmstopn  18472  metustexhalfOLD  18550  metustexhalf  18551  nlmnrg  18672  qdensere  18761  blcvx  18786  tgqioo  18788  icccmplem1  18810  icccmplem2  18811  reconnlem1  18814  cnmpt2pc  18910  iccpnfcnv  18926  phtpcer  18977  phtpcco2  18981  pcohtpy  19002  pcorev2  19010  pcophtb  19011  om1addcl  19015  pi1blem  19021  pi1cpbl  19026  pi1grplem  19031  pi1inv  19034  pi1xfrf  19035  pi1xfr  19037  pi1xfrcnvlem  19038  pi1cof  19041  pi1coghm  19043  cphreccllem  19098  cphsca  19099  cphsubrg  19100  cphsqrcl2  19106  tchclm  19146  tchcph  19151  lmmcvg  19171  cmetcaulem  19198  lmcau  19222  bcthlem3  19236  bcthlem4  19237  minveclem4c  19283  minveclem2  19284  minveclem3b  19286  minveclem4  19290  minveclem6  19292  ivthicc  19312  ovollb2lem  19341  ovolshftlem1  19362  ovolscalem1  19366  ovolicc1  19369  ovolicc2lem2  19371  ovolicc2lem3  19372  ovolicc2lem4  19373  ovolicc2lem5  19374  ioombl1lem1  19409  dyadmaxlem  19446  volivth  19456  vitalilem2  19458  vitalilem4  19460  i1fima2  19528  itg2monolem1  19599  itgcnlem  19638  itgrevallem1  19643  itgreval  19645  itgle  19658  ibladd  19669  iblabslem  19676  itgspliticc  19685  itgsplitioo  19686  ditgcl  19702  ditgswap  19703  ditgsplitlem  19704  limcdif  19720  limcresi  19729  limcres  19730  limccnp  19735  limccnp2  19736  limcun  19739  dvlip  19834  dvlip2  19836  dveq0  19841  dvgt0lem1  19843  dvivthlem1  19849  dvcnvrelem1  19858  dvcnvre  19860  dvfsumlem2  19868  ftc1lem1  19876  ftc1lem2  19877  ftc1a  19878  ftc1lem4  19880  ftc2  19885  ftc2ditglem  19886  itgsubstlem  19889  mpfind  19922  ply1rem  20043  fta1glem2  20046  ig1pdvds  20056  plyrem  20179  fta1lem  20181  vieta1lem2  20185  aaliou3lem3  20218  pserulm  20295  psercnlem2  20297  psercnlem1  20298  psercn  20299  pserdvlem1  20300  pserdvlem2  20301  abelth2  20315  coseq00topi  20367  coseq0negpitopi  20368  cosordlem  20390  tanord1  20396  efif1olem1  20401  dvloglem  20496  efopnlem1  20504  logreclem  20617  chordthmlem4  20633  quart1  20653  quartlem2  20655  quartlem3  20656  quart  20658  acosbnd  20697  atancj  20707  atanlogsublem  20712  atantan  20720  atanbndlem  20722  atans2  20728  dvatan  20732  atantayl  20734  divsqrsumlem  20775  ftalem5  20816  basellem5  20824  ppisval  20843  chtleppi  20951  chpchtsum  20960  chpub  20961  mersenne  20968  perfectlem2  20971  dchrinv  21002  rplogsumlem2  21136  chpdifbndlem1  21204  pntibndlem2  21242  pntlema  21247  pntlemb  21248  pntlemg  21249  pntlemh  21250  pntlemr  21253  pntlemj  21254  pntlemf  21256  pntlemk  21257  pntlemo  21258  pntlemp  21261  pntleml  21262  abvcxp  21266  ostth2lem2  21285  wlkonwlk  21492  eupapf  21651  tncp  21723  grpolidinv  21746  nvs  22108  nvz  22115  nvtri  22116  sspn  22192  minvecolem2  22334  minvecolem4c  22338  minvecolem4  22339  minvecolem5  22340  minvecolem6  22341  adj1  23393  eliccelico  24097  elicoelioo  24098  cnre2csqlem  24265  rnlogbval  24357  rnlogbcl  24358  nnlogbexp  24361  logbrec  24362  sigaclci  24472  unelsiga  24474  insiga  24477  measvun  24520  cntmeas  24537  sibfima  24610  sibfof  24611  subfacp1lem3  24825  subfacp1lem4  24826  subfacp1lem5  24827  sconpht2  24882  sconpi1  24883  txscon  24885  rescon  24890  cvmcn  24906  cvmsuni  24913  cvmsdisj  24914  cvmshmeo  24915  cvmlift2lem8  24954  cvmlift2lem13  24959  cvmliftphtlem  24961  cvmliftpht  24962  cvmlift3lem6  24968  ghomgrplem  25057  ibladdnc  26165  iblabsnclem  26171  ivthALT  26232  isbndx  26385  isbnd3  26387  prdsbnd  26396  heiborlem3  26416  iccbnd  26443  rngohomadd  26479  rngohommul  26480  idladdcl  26523  idllmulcl  26524  idlrmulcl  26525  maxidlmax  26547  pridlc  26575  acongrep  26939  pmtrfinv  27274  pmtrfmvdn0  27275  stoweidlem11  27631  stoweidlem31  27651  stoweidlem36  27656  stoweidlem38  27658  stoweidlem62  27682  sigardiv  27722  sigarcol  27725  sharhght  27726  sigaradd  27727  cevathlem1  27728  cevathlem2  27729  cevath  27730  el2wlksoton  28079  el2spthsoton  28080  bnj1018  29043  lshpnelb  29471  lshpcmp  29475  oplecon3  29686  opnoncon  29695  hlcvl  29846  dochshpncl  31871  lclkrslem1  32024  lclkrslem2  32025
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator