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

Theorem simp3d 969
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp3bi  972  oeeui  6687  erinxp  6820  resixp  6939  domssex2  7109  cantnflem1c  7479  cantnflem1  7481  cantnflem3  7483  cantnflem4  7484  fpwwe2lem7  8348  canthnumlem  8360  canthp1lem2  8365  wununi  8418  wunpw  8419  wunpr  8421  ixxdisj  10763  ixxun  10764  ixxss1  10766  ixxss2  10767  ixxss12  10768  ixxub  10769  ixxlb  10770  lbioo  10779  iccsupr  10828  icodisj  10853  xov1plusxeqvd  10872  intfracq  11055  fldiv  11056  seqf1olem2  11178  cjmul  11723  icco1  12110  rpnnen2lem10  12599  ruclem2  12607  ruclem3  12608  ruclem9  12613  ruclem12  12616  dvdslegcd  12792  crt  12943  eulerthlem1  12946  eulerthlem2  12947  pcpremul  12993  prmreclem2  13061  prmreclem3  13062  4sqlem13  13101  sectcan  13757  sectco  13758  sectmon  13779  monsect  13780  funcid  13843  funcco  13844  funcsect  13845  invfuc  13947  fuciso  13948  coapm  14002  catciso  14038  postr  14186  ipodrsima  14367  psref2  14412  psasym  14418  mhm0  14522  submcl  14529  submmnd  14530  eqger  14766  eqgcpbl  14770  gaorber  14861  orbsta  14866  cayleyth  14889  dfod2  14976  sylow2blem1  15030  sylow2blem3  15032  dprdcntz  15342  dprddisj  15343  dprdffi  15348  dpjdisj  15387  ablfac1a  15403  ablfac1b  15404  lmodvsdir  15751  lmhmlin  15891  lbsind  15932  2idlcpbl  16085  assasca  16161  mnfnei  17057  cnprcl  17081  lmcvg  17098  lmff  17135  lmcls  17136  lmcnp  17138  fbasssin  17633  flimfil  17766  tgpconcomp  17897  tlmtrg  17974  imasdsf1olem  18039  xmeter  18081  xmetresbl  18085  tmstopn  18133  nlmnrg  18292  qdensere  18381  blcvx  18406  tgqioo  18408  icccmplem1  18430  icccmplem2  18431  reconnlem1  18434  cnmpt2pc  18530  iccpnfcnv  18546  phtpcer  18597  phtpcco2  18601  pcohtpy  18622  pcorev2  18630  pcophtb  18631  om1addcl  18635  pi1blem  18641  pi1cpbl  18646  pi1grplem  18651  pi1inv  18654  pi1xfrf  18655  pi1xfr  18657  pi1xfrcnvlem  18658  pi1cof  18661  pi1coghm  18663  cphreccllem  18718  cphsca  18719  cphsubrg  18720  cphsqrcl2  18726  tchclm  18766  tchcph  18771  lmmcvg  18791  cmetcaulem  18818  lmcau  18842  bcthlem3  18852  bcthlem4  18853  minveclem4c  18893  minveclem2  18894  minveclem3b  18896  minveclem4  18900  minveclem6  18902  ivthicc  18922  ovollb2lem  18951  ovolshftlem1  18972  ovolscalem1  18976  ovolicc1  18979  ovolicc2lem2  18981  ovolicc2lem3  18982  ovolicc2lem4  18983  ovolicc2lem5  18984  ioombl1lem1  19019  dyadmaxlem  19056  volivth  19066  vitalilem2  19068  vitalilem4  19070  i1fima2  19138  itg2monolem1  19209  itgcnlem  19248  itgrevallem1  19253  itgreval  19255  itgle  19268  ibladd  19279  iblabslem  19286  itgspliticc  19295  itgsplitioo  19296  ditgcl  19312  ditgswap  19313  ditgsplitlem  19314  limcdif  19330  limcresi  19339  limcres  19340  limccnp  19345  limccnp2  19346  limcun  19349  dvlip  19444  dvlip2  19446  dveq0  19451  dvgt0lem1  19453  dvivthlem1  19459  dvcnvrelem1  19468  dvcnvre  19470  dvfsumlem2  19478  ftc1lem1  19486  ftc1lem2  19487  ftc1a  19488  ftc1lem4  19490  ftc2  19495  ftc2ditglem  19496  itgsubstlem  19499  mpfind  19532  ply1rem  19653  fta1glem2  19656  ig1pdvds  19666  plyrem  19789  fta1lem  19791  vieta1lem2  19795  aaliou3lem3  19828  pserulm  19905  psercnlem2  19907  psercnlem1  19908  psercn  19909  pserdvlem1  19910  pserdvlem2  19911  abelth2  19925  coseq00topi  19977  coseq0negpitopi  19978  cosordlem  20000  tanord1  20006  efif1olem1  20011  dvloglem  20106  efopnlem1  20114  logreclem  20227  chordthmlem4  20243  quart1  20263  quartlem2  20265  quartlem3  20266  quart  20268  acosbnd  20307  atancj  20317  atanlogsublem  20322  atantan  20330  atanbndlem  20332  atans2  20338  dvatan  20342  atantayl  20344  divsqrsumlem  20385  ftalem5  20426  basellem5  20434  ppisval  20453  chtleppi  20561  chpchtsum  20570  chpub  20571  mersenne  20578  perfectlem2  20581  dchrinv  20612  rplogsumlem2  20746  chpdifbndlem1  20814  pntibndlem2  20852  pntlema  20857  pntlemb  20858  pntlemg  20859  pntlemh  20860  pntlemr  20863  pntlemj  20864  pntlemf  20866  pntlemk  20867  pntlemo  20868  pntlemp  20871  pntleml  20872  abvcxp  20876  ostth2lem2  20895  tncp  20957  grpolidinv  20980  nvs  21342  nvz  21349  nvtri  21350  sspn  21426  minvecolem2  21568  minvecolem4c  21572  minvecolem4  21573  minvecolem5  21574  minvecolem6  21575  adj1  22627  eliccelico  23342  elicoelioo  23343  cnre2csqlem  23464  xrge0iifhom  23479  ustssel  23511  ustincl  23513  ustdiag  23514  ustinvel  23515  ustexhalf  23516  ustfilxp  23518  ustref  23522  tustopn  23569  tususp  23570  metustexhalf  23600  rnlogbval  23666  rnlogbcl  23667  nnlogbexp  23670  logbrec  23671  sigaclci  23781  unelsiga  23783  insiga  23786  measvun  23827  cntmeas  23844  subfacp1lem3  24117  subfacp1lem4  24118  subfacp1lem5  24119  sconpht2  24173  sconpi1  24174  txscon  24176  rescon  24181  cvmcn  24197  cvmsuni  24204  cvmsdisj  24205  cvmshmeo  24206  cvmlift2lem8  24245  cvmlift2lem13  24250  cvmliftphtlem  24252  cvmliftpht  24253  cvmlift3lem6  24259  eupapf  24291  ghomgrplem  24400  ibladdnc  25497  iblabsnclem  25503  ivthALT  25582  isbndx  25829  isbnd3  25831  prdsbnd  25840  heiborlem3  25860  iccbnd  25887  rngohomadd  25923  rngohommul  25924  idladdcl  25967  idllmulcl  25968  idlrmulcl  25969  maxidlmax  25991  pridlc  26019  acongrep  26390  pmtrfinv  26725  pmtrfmvdn0  26726  stoweidlem11  27083  stoweidlem31  27103  stoweidlem36  27108  stoweidlem62  27134  sigardiv  27174  sigarcol  27177  sharhght  27178  sigaradd  27179  cevathlem1  27180  cevathlem2  27181  cevath  27182  wlkonwlk  27687  bnj1018  28756  lshpnelb  29243  lshpcmp  29247  oplecon3  29458  opnoncon  29467  hlcvl  29618  dochshpncl  31643  lclkrslem1  31796  lclkrslem2  31797
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 936
  Copyright terms: Public domain W3C validator