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  6602  erinxp  6735  resixp  6853  domssex2  7023  cantnflem1c  7391  cantnflem1  7393  cantnflem3  7395  cantnflem4  7396  fpwwe2lem7  8260  canthnumlem  8272  canthp1lem2  8277  wununi  8330  wunpw  8331  wunpr  8333  ixxdisj  10673  ixxun  10674  ixxss1  10676  ixxss2  10677  ixxss12  10678  ixxub  10679  ixxlb  10680  lbioo  10689  iccsupr  10738  icodisj  10763  xov1plusxeqvd  10782  intfracq  10965  fldiv  10966  seqf1olem2  11088  cjmul  11629  icco1  12016  rpnnen2lem10  12504  ruclem2  12512  ruclem3  12513  ruclem9  12518  ruclem12  12521  dvdslegcd  12697  crt  12848  eulerthlem1  12851  eulerthlem2  12852  pcpremul  12898  prmreclem2  12966  prmreclem3  12967  4sqlem13  13006  sectcan  13660  sectco  13661  sectmon  13682  monsect  13683  funcid  13746  funcco  13747  funcsect  13748  invfuc  13850  fuciso  13851  coapm  13905  catciso  13941  postr  14089  ipodrsima  14270  psref2  14315  psasym  14321  mhm0  14425  submcl  14432  submmnd  14433  eqger  14669  eqgcpbl  14673  gaorber  14764  orbsta  14769  cayleyth  14792  dfod2  14879  sylow2blem1  14933  sylow2blem3  14935  dprdcntz  15245  dprddisj  15246  dprdffi  15251  dpjdisj  15290  ablfac1a  15306  ablfac1b  15307  lmodvsdir  15654  lmhmlin  15794  lbsind  15835  2idlcpbl  15988  assasca  16064  mnfnei  16953  cnprcl  16977  lmcvg  16994  lmff  17031  lmcls  17032  lmcnp  17034  fbasssin  17533  flimfil  17666  tgpconcomp  17797  tlmtrg  17874  imasdsf1olem  17939  xmeter  17981  xmetresbl  17985  tmstopn  18033  nlmnrg  18192  qdensere  18281  blcvx  18306  tgqioo  18308  icccmplem1  18329  icccmplem2  18330  reconnlem1  18333  cnmpt2pc  18428  iccpnfcnv  18444  phtpcer  18495  phtpcco2  18499  pcohtpy  18520  pcorev2  18528  pcophtb  18529  om1addcl  18533  pi1blem  18539  pi1cpbl  18544  pi1grplem  18549  pi1inv  18552  pi1xfrf  18553  pi1xfr  18555  pi1xfrcnvlem  18556  pi1cof  18559  pi1coghm  18561  cphreccllem  18616  cphsca  18617  cphsubrg  18618  cphsqrcl2  18624  tchclm  18664  tchcph  18669  lmmcvg  18689  cmetcaulem  18716  lmcau  18740  bcthlem3  18750  bcthlem4  18751  minveclem4c  18791  minveclem2  18792  minveclem3b  18794  minveclem4  18798  minveclem6  18800  ivthicc  18820  ovollb2lem  18849  ovolshftlem1  18870  ovolscalem1  18874  ovolicc1  18877  ovolicc2lem2  18879  ovolicc2lem3  18880  ovolicc2lem4  18881  ovolicc2lem5  18882  ioombl1lem1  18917  dyadmaxlem  18954  volivth  18964  vitalilem2  18966  vitalilem4  18968  i1fima2  19036  itg2monolem1  19107  itgcnlem  19146  itgrevallem1  19151  itgreval  19153  itgle  19166  ibladd  19177  iblabslem  19184  itgspliticc  19193  itgsplitioo  19194  ditgcl  19210  ditgswap  19211  ditgsplitlem  19212  limcdif  19228  limcresi  19237  limcres  19238  limccnp  19243  limccnp2  19244  limcun  19247  dvlip  19342  dvlip2  19344  dveq0  19349  dvgt0lem1  19351  dvivthlem1  19357  dvcnvrelem1  19366  dvcnvre  19368  dvfsumlem2  19376  ftc1lem1  19384  ftc1lem2  19385  ftc1a  19386  ftc1lem4  19388  ftc2  19393  ftc2ditglem  19394  itgsubstlem  19397  mpfind  19430  ply1rem  19551  fta1glem2  19554  ig1pdvds  19564  plyrem  19687  fta1lem  19689  vieta1lem2  19693  aaliou3lem3  19726  pserulm  19800  psercnlem2  19802  psercnlem1  19803  psercn  19804  pserdvlem1  19805  pserdvlem2  19806  abelth2  19820  coseq00topi  19872  coseq0negpitopi  19873  cosordlem  19895  tanord1  19901  efif1olem1  19906  dvloglem  19997  efopnlem1  20005  logreclem  20118  chordthmlem4  20134  quart1  20154  quartlem2  20156  quartlem3  20157  quart  20159  acosbnd  20198  atancj  20208  atanlogsublem  20213  atantan  20221  atanbndlem  20223  atans2  20229  dvatan  20233  atantayl  20235  divsqrsumlem  20276  ftalem5  20316  basellem5  20324  ppisval  20343  chtleppi  20451  chpchtsum  20460  chpub  20461  mersenne  20468  perfectlem2  20471  dchrinv  20502  rplogsumlem2  20636  chpdifbndlem1  20704  pntibndlem2  20742  pntlema  20747  pntlemb  20748  pntlemg  20749  pntlemh  20750  pntlemr  20753  pntlemj  20754  pntlemf  20756  pntlemk  20757  pntlemo  20758  pntlemp  20761  pntleml  20762  abvcxp  20766  ostth2lem2  20785  tncp  20847  grpolidinv  20870  nvs  21230  nvz  21237  nvtri  21238  sspn  21314  minvecolem2  21456  minvecolem4c  21460  minvecolem4  21461  minvecolem5  21462  minvecolem6  21463  adj1  22515  eliccelico  23272  elicoelioo  23273  cnre2csqlem  23296  xrge0iifhom  23321  rnlogbval  23404  rnlogbcl  23405  nnlogbexp  23408  logbrec  23409  sigaclci  23495  unelsiga  23497  insiga  23500  measvun  23539  cntmeas  23555  subfacp1lem3  23715  subfacp1lem4  23716  subfacp1lem5  23717  sconpht2  23771  sconpi1  23772  txscon  23774  rescon  23779  cvmcn  23795  cvmsuni  23802  cvmsdisj  23803  cvmshmeo  23804  cvmlift2lem8  23843  cvmlift2lem13  23848  cvmliftphtlem  23850  cvmliftpht  23851  cvmlift3lem6  23857  eupapf  23889  ghomgrplem  23998  preoref12  25239  fldax6  25444  fldax7  25445  vecax3  25466  vecax4  25467  vecax5  25468  vecax6  25469  icccon3  25712  ida  25741  cmpmorp  25790  dualalg  25793  cehm  25804  fmp  25851  prismorcset3  25949  rocatval  25970  ivthALT  26269  isbndx  26517  isbnd3  26519  prdsbnd  26528  heiborlem3  26548  iccbnd  26575  rngohomadd  26611  rngohommul  26612  idladdcl  26655  idllmulcl  26656  idlrmulcl  26657  maxidlmax  26679  pridlc  26707  acongrep  27078  pmtrfinv  27413  pmtrfmvdn0  27414  stoweidlem11  27771  stoweidlem31  27791  stoweidlem36  27796  stoweidlem62  27822  sigardiv  27862  sigarcol  27865  sharhght  27866  sigaradd  27867  cevathlem1  27868  cevathlem2  27869  cevath  27870  bnj1018  29067  lshpnelb  29247  lshpcmp  29251  oplecon3  29462  opnoncon  29471  hlcvl  29622  dochshpncl  31647  lclkrslem1  31800  lclkrslem2  31801
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