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  6600  erinxp  6733  resixp  6851  domssex2  7021  cantnflem1c  7389  cantnflem1  7391  cantnflem3  7393  cantnflem4  7394  fpwwe2lem7  8258  canthnumlem  8270  canthp1lem2  8275  wununi  8328  wunpw  8329  wunpr  8331  ixxdisj  10671  ixxun  10672  ixxss1  10674  ixxss2  10675  ixxss12  10676  ixxub  10677  ixxlb  10678  lbioo  10687  iccsupr  10736  icodisj  10761  xov1plusxeqvd  10780  intfracq  10963  fldiv  10964  seqf1olem2  11086  cjmul  11627  icco1  12014  rpnnen2lem10  12502  ruclem2  12510  ruclem3  12511  ruclem9  12516  ruclem12  12519  dvdslegcd  12695  crt  12846  eulerthlem1  12849  eulerthlem2  12850  pcpremul  12896  prmreclem2  12964  prmreclem3  12965  4sqlem13  13004  sectcan  13658  sectco  13659  sectmon  13680  monsect  13681  funcid  13744  funcco  13745  funcsect  13746  invfuc  13848  fuciso  13849  coapm  13903  catciso  13939  postr  14087  ipodrsima  14268  psref2  14313  psasym  14319  mhm0  14423  submcl  14430  submmnd  14431  eqger  14667  eqgcpbl  14671  gaorber  14762  orbsta  14767  cayleyth  14790  dfod2  14877  sylow2blem1  14931  sylow2blem3  14933  dprdcntz  15243  dprddisj  15244  dprdffi  15249  dpjdisj  15288  ablfac1a  15304  ablfac1b  15305  lmodvsdir  15652  lmhmlin  15792  lbsind  15833  2idlcpbl  15986  assasca  16062  mnfnei  16951  cnprcl  16975  lmcvg  16992  lmff  17029  lmcls  17030  lmcnp  17032  fbasssin  17531  flimfil  17664  tgpconcomp  17795  tlmtrg  17872  imasdsf1olem  17937  xmeter  17979  xmetresbl  17983  tmstopn  18031  nlmnrg  18190  qdensere  18279  blcvx  18304  tgqioo  18306  icccmplem1  18327  icccmplem2  18328  reconnlem1  18331  cnmpt2pc  18426  iccpnfcnv  18442  phtpcer  18493  phtpcco2  18497  pcohtpy  18518  pcorev2  18526  pcophtb  18527  om1addcl  18531  pi1blem  18537  pi1cpbl  18542  pi1grplem  18547  pi1inv  18550  pi1xfrf  18551  pi1xfr  18553  pi1xfrcnvlem  18554  pi1cof  18557  pi1coghm  18559  cphreccllem  18614  cphsca  18615  cphsubrg  18616  cphsqrcl2  18622  tchclm  18662  tchcph  18667  lmmcvg  18687  cmetcaulem  18714  lmcau  18738  bcthlem3  18748  bcthlem4  18749  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  ivthicc  18818  ovollb2lem  18847  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem2  18877  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1lem1  18915  dyadmaxlem  18952  volivth  18962  vitalilem2  18964  vitalilem4  18966  i1fima2  19034  itg2monolem1  19105  itgcnlem  19144  itgrevallem1  19149  itgreval  19151  itgle  19164  ibladd  19175  iblabslem  19182  itgspliticc  19191  itgsplitioo  19192  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  limcdif  19226  limcresi  19235  limcres  19236  limccnp  19241  limccnp2  19242  limcun  19245  dvlip  19340  dvlip2  19342  dveq0  19347  dvgt0lem1  19349  dvivthlem1  19355  dvcnvrelem1  19364  dvcnvre  19366  dvfsumlem2  19374  ftc1lem1  19382  ftc1lem2  19383  ftc1a  19384  ftc1lem4  19386  ftc2  19391  ftc2ditglem  19392  itgsubstlem  19395  mpfind  19428  ply1rem  19549  fta1glem2  19552  ig1pdvds  19562  plyrem  19685  fta1lem  19687  vieta1lem2  19691  aaliou3lem3  19724  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  abelth2  19818  coseq00topi  19870  coseq0negpitopi  19871  cosordlem  19893  tanord1  19899  efif1olem1  19904  dvloglem  19995  efopnlem1  20003  logreclem  20116  chordthmlem4  20132  quart1  20152  quartlem2  20154  quartlem3  20155  quart  20157  acosbnd  20196  atancj  20206  atanlogsublem  20211  atantan  20219  atanbndlem  20221  atans2  20227  dvatan  20231  atantayl  20233  divsqrsumlem  20274  ftalem5  20314  basellem5  20322  ppisval  20341  chtleppi  20449  chpchtsum  20458  chpub  20459  mersenne  20466  perfectlem2  20469  dchrinv  20500  rplogsumlem2  20634  chpdifbndlem1  20702  pntibndlem2  20740  pntlema  20745  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlemp  20759  pntleml  20760  abvcxp  20764  ostth2lem2  20783  tncp  20845  grpolidinv  20868  nvs  21228  nvz  21235  nvtri  21236  sspn  21312  minvecolem2  21454  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  adj1  22513  eliccelico  23270  elicoelioo  23271  cnre2csqlem  23294  xrge0iifhom  23319  rnlogbval  23402  rnlogbcl  23403  nnlogbexp  23406  logbrec  23407  sigaclci  23493  unelsiga  23495  insiga  23498  measvun  23537  cntmeas  23553  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  sconpht2  23769  sconpi1  23770  txscon  23772  rescon  23777  cvmcn  23793  cvmsuni  23800  cvmsdisj  23801  cvmshmeo  23802  cvmlift2lem8  23841  cvmlift2lem13  23846  cvmliftphtlem  23848  cvmliftpht  23849  cvmlift3lem6  23855  eupapf  23887  ghomgrplem  23996  preoref12  25228  fldax6  25433  fldax7  25434  vecax3  25455  vecax4  25456  vecax5  25457  vecax6  25458  icccon3  25701  ida  25730  cmpmorp  25779  dualalg  25782  cehm  25793  fmp  25840  prismorcset3  25938  rocatval  25959  ivthALT  26258  isbndx  26506  isbnd3  26508  prdsbnd  26517  heiborlem3  26537  iccbnd  26564  rngohomadd  26600  rngohommul  26601  idladdcl  26644  idllmulcl  26645  idlrmulcl  26646  maxidlmax  26668  pridlc  26696  acongrep  27067  pmtrfinv  27402  pmtrfmvdn0  27403  stoweidlem11  27760  stoweidlem31  27780  stoweidlem36  27785  stoweidlem62  27811  sigardiv  27851  sigarcol  27854  sharhght  27855  sigaradd  27856  cevathlem1  27857  cevathlem2  27858  cevath  27859  bnj1018  28994  lshpnelb  29174  lshpcmp  29178  oplecon3  29389  opnoncon  29398  hlcvl  29549  dochshpncl  31574  lclkrslem1  31727  lclkrslem2  31728
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