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  6836  erinxp  6969  resixp  7088  domssex2  7258  cantnflem1c  7632  cantnflem1  7634  cantnflem3  7636  cantnflem4  7637  fpwwe2lem7  8500  canthnumlem  8512  canthp1lem2  8517  wununi  8570  wunpw  8571  wunpr  8573  ixxdisj  10920  ixxun  10921  ixxss1  10923  ixxss2  10924  ixxss12  10925  ixxub  10926  ixxlb  10927  lbioo  10936  iccsupr  10986  icodisj  11011  xov1plusxeqvd  11030  intfracq  11228  fldiv  11229  seqf1olem2  11351  cjmul  11935  icco1  12322  rpnnen2lem10  12811  ruclem2  12819  ruclem3  12820  ruclem9  12825  ruclem12  12828  dvdslegcd  13004  crt  13155  eulerthlem1  13158  eulerthlem2  13159  pcpremul  13205  prmreclem2  13273  prmreclem3  13274  4sqlem13  13313  sectcan  13969  sectco  13970  sectmon  13991  monsect  13992  funcid  14055  funcco  14056  funcsect  14057  invfuc  14159  fuciso  14160  coapm  14214  catciso  14250  postr  14398  ipodrsima  14579  psref2  14624  psasym  14630  mhm0  14734  submcl  14741  submmnd  14742  eqger  14978  eqgcpbl  14982  gaorber  15073  orbsta  15078  cayleyth  15101  dfod2  15188  sylow2blem1  15242  sylow2blem3  15244  dprdcntz  15554  dprddisj  15555  dprdffi  15560  dpjdisj  15599  ablfac1a  15615  ablfac1b  15616  lmodvsdir  15962  lmhmlin  16099  lbsind  16140  2idlcpbl  16293  assasca  16369  mnfnei  17273  cnprcl  17297  lmcvg  17314  lmff  17353  lmcls  17354  lmcnp  17356  fbasssin  17856  flimfil  17989  tgpconcomp  18130  tlmtrg  18207  ustssel  18223  ustincl  18225  ustdiag  18226  ustinvel  18227  ustexhalf  18228  ustfilxp  18230  tustopn  18289  tususp  18290  imasdsf1olem  18391  xmeter  18451  xmetresbl  18455  tmstopn  18503  metustexhalfOLD  18581  metustexhalf  18582  nlmnrg  18703  qdensere  18792  blcvx  18817  tgqioo  18819  icccmplem1  18841  icccmplem2  18842  reconnlem1  18845  cnmpt2pc  18941  iccpnfcnv  18957  phtpcer  19008  phtpcco2  19012  pcohtpy  19033  pcorev2  19041  pcophtb  19042  om1addcl  19046  pi1blem  19052  pi1cpbl  19057  pi1grplem  19062  pi1inv  19065  pi1xfrf  19066  pi1xfr  19068  pi1xfrcnvlem  19069  pi1cof  19072  pi1coghm  19074  cphreccllem  19129  cphsca  19130  cphsubrg  19131  cphsqrcl2  19137  tchclm  19177  tchcph  19182  lmmcvg  19202  cmetcaulem  19229  lmcau  19253  bcthlem3  19267  bcthlem4  19268  minveclem4c  19314  minveclem2  19315  minveclem3b  19317  minveclem4  19321  minveclem6  19323  ivthicc  19343  ovollb2lem  19372  ovolshftlem1  19393  ovolscalem1  19397  ovolicc1  19400  ovolicc2lem2  19402  ovolicc2lem3  19403  ovolicc2lem4  19404  ovolicc2lem5  19405  ioombl1lem1  19440  dyadmaxlem  19477  volivth  19487  vitalilem2  19489  vitalilem4  19491  i1fima2  19559  itg2monolem1  19630  itgcnlem  19669  itgrevallem1  19674  itgreval  19676  itgle  19689  ibladd  19700  iblabslem  19707  itgspliticc  19716  itgsplitioo  19717  ditgcl  19733  ditgswap  19734  ditgsplitlem  19735  limcdif  19751  limcresi  19760  limcres  19761  limccnp  19766  limccnp2  19767  limcun  19770  dvlip  19865  dvlip2  19867  dveq0  19872  dvgt0lem1  19874  dvivthlem1  19880  dvcnvrelem1  19889  dvcnvre  19891  dvfsumlem2  19899  ftc1lem1  19907  ftc1lem2  19908  ftc1a  19909  ftc1lem4  19911  ftc2  19916  ftc2ditglem  19917  itgsubstlem  19920  mpfind  19953  ply1rem  20074  fta1glem2  20077  ig1pdvds  20087  plyrem  20210  fta1lem  20212  vieta1lem2  20216  aaliou3lem3  20249  pserulm  20326  psercnlem2  20328  psercnlem1  20329  psercn  20330  pserdvlem1  20331  pserdvlem2  20332  abelth2  20346  coseq00topi  20398  coseq0negpitopi  20399  cosordlem  20421  tanord1  20427  efif1olem1  20432  dvloglem  20527  efopnlem1  20535  logreclem  20648  chordthmlem4  20664  quart1  20684  quartlem2  20686  quartlem3  20687  quart  20689  acosbnd  20728  atancj  20738  atanlogsublem  20743  atantan  20751  atanbndlem  20753  atans2  20759  dvatan  20763  atantayl  20765  divsqrsumlem  20806  ftalem5  20847  basellem5  20855  ppisval  20874  chtleppi  20982  chpchtsum  20991  chpub  20992  mersenne  20999  perfectlem2  21002  dchrinv  21033  rplogsumlem2  21167  chpdifbndlem1  21235  pntibndlem2  21273  pntlema  21278  pntlemb  21279  pntlemg  21280  pntlemh  21281  pntlemr  21284  pntlemj  21285  pntlemf  21287  pntlemk  21288  pntlemo  21289  pntlemp  21292  pntleml  21293  abvcxp  21297  ostth2lem2  21316  wlkonwlk  21523  eupapf  21682  tncp  21754  grpolidinv  21777  nvs  22139  nvz  22146  nvtri  22147  sspn  22223  minvecolem2  22365  minvecolem4c  22369  minvecolem4  22370  minvecolem5  22371  minvecolem6  22372  adj1  23424  eliccelico  24128  elicoelioo  24129  cnre2csqlem  24296  rnlogbval  24388  rnlogbcl  24389  nnlogbexp  24392  logbrec  24393  sigaclci  24503  unelsiga  24505  insiga  24508  measvun  24551  cntmeas  24568  sibfima  24641  sibfof  24642  subfacp1lem3  24856  subfacp1lem4  24857  subfacp1lem5  24858  sconpht2  24913  sconpi1  24914  txscon  24916  rescon  24921  cvmcn  24937  cvmsuni  24944  cvmsdisj  24945  cvmshmeo  24946  cvmlift2lem8  24985  cvmlift2lem13  24990  cvmliftphtlem  24992  cvmliftpht  24993  cvmlift3lem6  24999  ghomgrplem  25088  ibladdnc  26208  iblabsnclem  26214  ivthALT  26275  isbndx  26428  isbnd3  26430  prdsbnd  26439  heiborlem3  26459  iccbnd  26486  rngohomadd  26522  rngohommul  26523  idladdcl  26566  idllmulcl  26567  idlrmulcl  26568  maxidlmax  26590  pridlc  26618  acongrep  26982  pmtrfinv  27317  pmtrfmvdn0  27318  stoweidlem11  27674  stoweidlem31  27694  stoweidlem36  27699  stoweidlem38  27701  stoweidlem62  27725  sigardiv  27765  sigarcol  27768  sharhght  27769  sigaradd  27770  cevathlem1  27771  cevathlem2  27772  cevath  27773  shwrdssizelem1a  28165  el2wlksoton  28219  el2spthsoton  28220  bnj1018  29187  lshpnelb  29621  lshpcmp  29625  oplecon3  29836  opnoncon  29845  hlcvl  29996  dochshpncl  32021  lclkrslem1  32174  lclkrslem2  32175
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