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  6596  erinxp  6729  resixp  6847  domssex2  7017  cantnflem1c  7385  cantnflem1  7387  cantnflem3  7389  cantnflem4  7390  fpwwe2lem7  8254  canthnumlem  8266  canthp1lem2  8271  wununi  8324  wunpw  8325  wunpr  8327  ixxdisj  10667  ixxun  10668  ixxss1  10670  ixxss2  10671  ixxss12  10672  ixxub  10673  ixxlb  10674  lbioo  10683  iccsupr  10732  icodisj  10757  xov1plusxeqvd  10776  intfracq  10959  fldiv  10960  seqf1olem2  11082  cjmul  11623  icco1  12010  rpnnen2lem10  12498  ruclem2  12506  ruclem3  12507  ruclem9  12512  ruclem12  12515  dvdslegcd  12691  crt  12842  eulerthlem1  12845  eulerthlem2  12846  pcpremul  12892  prmreclem2  12960  prmreclem3  12961  4sqlem13  13000  sectcan  13654  sectco  13655  sectmon  13676  monsect  13677  funcid  13740  funcco  13741  funcsect  13742  invfuc  13844  fuciso  13845  coapm  13899  catciso  13935  postr  14083  ipodrsima  14264  psref2  14309  psasym  14315  mhm0  14419  submcl  14426  submmnd  14427  eqger  14663  eqgcpbl  14667  gaorber  14758  orbsta  14763  cayleyth  14786  dfod2  14873  sylow2blem1  14927  sylow2blem3  14929  dprdcntz  15239  dprddisj  15240  dprdffi  15245  dpjdisj  15284  ablfac1a  15300  ablfac1b  15301  lmodvsdir  15648  lmhmlin  15788  lbsind  15829  2idlcpbl  15982  assasca  16058  mnfnei  16947  cnprcl  16971  lmcvg  16988  lmff  17025  lmcls  17026  lmcnp  17028  fbasssin  17527  flimfil  17660  tgpconcomp  17791  tlmtrg  17868  imasdsf1olem  17933  xmeter  17975  xmetresbl  17979  tmstopn  18027  nlmnrg  18186  qdensere  18275  blcvx  18300  tgqioo  18302  icccmplem1  18323  icccmplem2  18324  reconnlem1  18327  cnmpt2pc  18422  iccpnfcnv  18438  phtpcer  18489  phtpcco2  18493  pcohtpy  18514  pcorev2  18522  pcophtb  18523  om1addcl  18527  pi1blem  18533  pi1cpbl  18538  pi1grplem  18543  pi1inv  18546  pi1xfrf  18547  pi1xfr  18549  pi1xfrcnvlem  18550  pi1cof  18553  pi1coghm  18555  cphreccllem  18610  cphsca  18611  cphsubrg  18612  cphsqrcl2  18618  tchclm  18658  tchcph  18663  lmmcvg  18683  cmetcaulem  18710  lmcau  18734  bcthlem3  18744  bcthlem4  18745  minveclem4c  18785  minveclem2  18786  minveclem3b  18788  minveclem4  18792  minveclem6  18794  ivthicc  18814  ovollb2lem  18843  ovolshftlem1  18864  ovolscalem1  18868  ovolicc1  18871  ovolicc2lem2  18873  ovolicc2lem3  18874  ovolicc2lem4  18875  ovolicc2lem5  18876  ioombl1lem1  18911  dyadmaxlem  18948  volivth  18958  vitalilem2  18960  vitalilem4  18962  i1fima2  19030  itg2monolem1  19101  itgcnlem  19140  itgrevallem1  19145  itgreval  19147  itgle  19160  ibladd  19171  iblabslem  19178  itgspliticc  19187  itgsplitioo  19188  ditgcl  19204  ditgswap  19205  ditgsplitlem  19206  limcdif  19222  limcresi  19231  limcres  19232  limccnp  19237  limccnp2  19238  limcun  19241  dvlip  19336  dvlip2  19338  dveq0  19343  dvgt0lem1  19345  dvivthlem1  19351  dvcnvrelem1  19360  dvcnvre  19362  dvfsumlem2  19370  ftc1lem1  19378  ftc1lem2  19379  ftc1a  19380  ftc1lem4  19382  ftc2  19387  ftc2ditglem  19388  itgsubstlem  19391  mpfind  19424  ply1rem  19545  fta1glem2  19548  ig1pdvds  19558  plyrem  19681  fta1lem  19683  vieta1lem2  19687  aaliou3lem3  19720  pserulm  19794  psercnlem2  19796  psercnlem1  19797  psercn  19798  pserdvlem1  19799  pserdvlem2  19800  abelth2  19814  coseq00topi  19866  coseq0negpitopi  19867  cosordlem  19889  tanord1  19895  efif1olem1  19900  dvloglem  19991  efopnlem1  19999  logreclem  20112  chordthmlem4  20128  quart1  20148  quartlem2  20150  quartlem3  20151  quart  20153  acosbnd  20192  atancj  20202  atanlogsublem  20207  atantan  20215  atanbndlem  20217  atans2  20223  dvatan  20227  atantayl  20229  divsqrsumlem  20270  ftalem5  20310  basellem5  20318  ppisval  20337  chtleppi  20445  chpchtsum  20454  chpub  20455  mersenne  20462  perfectlem2  20465  dchrinv  20496  rplogsumlem2  20630  chpdifbndlem1  20698  pntibndlem2  20736  pntlema  20741  pntlemb  20742  pntlemg  20743  pntlemh  20744  pntlemr  20747  pntlemj  20748  pntlemf  20750  pntlemk  20751  pntlemo  20752  pntlemp  20755  pntleml  20756  abvcxp  20760  ostth2lem2  20779  tncp  20839  grpolidinv  20862  nvs  21222  nvz  21229  nvtri  21230  sspn  21306  minvecolem2  21448  minvecolem4c  21452  minvecolem4  21453  minvecolem5  21454  minvecolem6  21455  adj1  22509  subfacp1lem3  23120  subfacp1lem4  23121  subfacp1lem5  23122  sconpht2  23176  sconpi1  23177  txscon  23179  rescon  23184  cvmcn  23200  cvmsuni  23207  cvmsdisj  23208  cvmshmeo  23209  cvmlift2lem8  23248  cvmlift2lem13  23253  cvmliftphtlem  23255  cvmliftpht  23256  cvmlift3lem6  23262  eupapf  23294  ghomgrplem  23403  preoref12  24639  fldax6  24844  fldax7  24845  vecax3  24866  vecax4  24867  vecax5  24868  vecax6  24869  icccon3  25112  ida  25141  cmpmorp  25190  dualalg  25193  cehm  25204  fmp  25251  prismorcset3  25349  rocatval  25370  ivthALT  25669  isbndx  25917  isbnd3  25919  prdsbnd  25928  heiborlem3  25948  iccbnd  25975  rngohomadd  26011  rngohommul  26012  idladdcl  26055  idllmulcl  26056  idlrmulcl  26057  maxidlmax  26079  pridlc  26107  acongrep  26478  pmtrfinv  26813  pmtrfmvdn0  26814  stoweidlem11  27171  stoweidlem31  27191  stoweidlem36  27196  stoweidlem62  27222  bnj1018  28273  lshpnelb  28453  lshpcmp  28457  oplecon3  28668  opnoncon  28677  hlcvl  28828  dochshpncl  30853  lclkrslem1  31006  lclkrslem2  31007
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