Theorem simp2d 1008

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
simp2d	|- ( ph -> ch )

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp2 996	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 16	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ w3a 972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974

This theorem is referenced by:  simp2bi  1011  f1dom3fv3dif  6156  f1dom3el3dif  6157  oeeui  7249  erinxp  7383  resixp  7502  domssex  7676  cantnflem1a  8102  cantnflem1d  8105  cantnflem3  8108  cantnflem4  8109  cantnflem1aOLD  8125  cantnflem1dOLD  8128  cantnflem3OLD  8130  cantnflem4OLD  8131  fpwwe2lem7  9012  canthnumlem  9024  canthp1lem2  9029  wun0  9094  supmullem2  10511  supmul  10512  ixxdisj  11548  ixxun  11549  ixxss1  11551  ixxss2  11552  ixxss12  11553  ixxub  11554  ixxlb  11555  ubioo  11565  iccgelb  11585  iccss2  11599  icodisj  11649  xov1plusxeqvd  11670  fldiv  11961  immul  12943  sqrtge0  13065  sqrtrege0  13172  icco1  13337  ruclem2  13837  ruclem3  13838  ruclem8  13842  ruclem12  13846  gcddvds  14025  crt  14180  phimullem  14181  eulerthlem1  14183  eulerthlem2  14184  prmreclem3  14308  sectcan  15022  sectco  15023  sectmon  15044  monsect  15045  funcixp  15105  funcsect  15110  invfuc  15212  coapm  15267  catciso  15303  posasymb  15451  ipodrsima  15664  pstr2  15704  psdmrn  15706  psref  15707  mhmlin  15842  subm0cl  15852  eqger  16120  eqgcpbl  16124  gaorber  16215  orbstafun  16218  cayleyth  16309  pmtrrn2  16354  pmtrfinv  16355  dfod2  16455  sylow2blem1  16509  dprdf  16908  dprdff  16914  dprdfcl  16915  dprdffOLD  16920  dprdfclOLD  16921  dprdsplit  16965  dpjcntz  16969  ablfac1a  16988  ablfac1b  16989  lmodvsdi  17403  lbssp  17593  2idlcpbl  17750  assaring  17837  mpff  18070  mpfaddcl  18071  mpfmulcl  18072  mpfind  18073  pf1rcl  18253  mpfpf1  18255  mdetunilem2  18982  mdetunilem5  18985  mdetunilem6  18986  chfacfisfcpmat  19223  pnfnei  19587  cnptop2  19610  lmcl  19664  lmcnp  19671  flimfil  20336  tlmlmod  20557  ustbasel  20575  ustincl  20576  ustinvel  20578  ustfilxp  20581  tusunif  20638  imasdsf1olem  20742  xmeter  20802  tmsds  20853  metustexhalfOLD  20932  metustexhalf  20933  nlmlmod  21053  qdensere  21143  blcvx  21169  tgqioo  21171  icccmplem2  21194  reconnlem1  21197  cnmpt2pc  21294  phtpcer  21361  phtpcco2  21365  pcohtpylem  21385  pcohtpy  21386  pcophtb  21395  om1addcl  21399  pi1blem  21405  pi1cpbl  21410  pi1grplem  21415  pi1inv  21418  pi1xfrf  21419  pi1xfr  21421  pi1xfrcnvlem  21422  pi1cof  21425  pi1coghm  21427  cphnlm  21485  cphsqrtcl2  21499  tchcph  21546  lmcau  21617  bcthlem4  21632  minveclem4c  21706  minveclem2  21707  minveclem3b  21709  minveclem4  21713  minveclem6  21715  ivthicc  21736  ovolfsval  21748  ovollb2lem  21765  ovolshftlem1  21786  ovolscalem1  21790  ovolicc1  21793  ovolicc2lem2  21795  ovolicc2lem4  21797  ovolicc2lem5  21798  ovolicopnf  21801  ioombl1lem1  21834  ioombl1lem3  21836  ioombl1lem4  21837  uniioovol  21854  uniioombllem2a  21857  uniioombllem2  21858  uniioombllem3a  21859  uniioombllem3  21860  uniioombllem4  21861  uniioombllem6  21863  dyadmaxlem  21872  volivth  21882  vitalilem2  21884  vitalilem5  21887  i1frn  21950  itg2monolem1  22023  itgcnlem  22062  itgrevallem1  22067  itgreval  22069  itgle  22082  ibladd  22093  iblabslem  22100  itgspliticc  22109  itgsplitioo  22110  ditgcl  22128  ditgswap  22129  ditgsplitlem  22130  limcdif  22146  limcresi  22155  limccnp  22161  limccnp2  22162  limcco  22163  dvlip  22260  dvlip2  22262  dveq0  22267  dvgt0lem1  22269  dvivthlem1  22275  dvcnvrelem1  22284  dvcnvre  22286  dvfsumlem2  22294  ftc1lem1  22302  ftc1a  22304  ftc1lem4  22306  ftc2ditglem  22312  itgsubstlem  22315  ply1rem  22430  fta1glem1  22432  ig1pdvds  22443  plyrem  22566  facth  22567  fta1lem  22568  vieta1lem1  22571  vieta1lem2  22572  aaliou3lem3  22605  aaliou3lem4  22607  aaliou3lem7  22610  taylfvallem1  22617  tayl0  22622  taylply2  22628  radcnvle  22680  psercnlem2  22684  psercnlem1  22685  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  abelth2  22702  coseq00topi  22760  coseq0negpitopi  22761  cosordlem  22783  tanord1  22789  efif1olem1  22794  loglesqrt  22997  logreclem  23015  chordthmlem4  23031  quart1  23052  quartlem2  23054  quartlem3  23055  quartlem4  23056  quart  23057  acosbnd  23096  atancj  23106  atanlogsublem  23111  atantan  23119  atanbndlem  23121  dvatan  23131  atantayl  23133  rlimcnp2  23161  divsqrtsumlem  23174  ftalem5  23215  ftalem7  23217  basellem4  23222  basellem5  23223  perfectlem2  23370  dchrinv  23401  chpdifbndlem1  23603  pntibndlem2  23641  pntlemc  23645  pntlema  23646  pntlemb  23647  pntlemg  23648  pntlemh  23649  pntlemq  23651  pntlemr  23652  pntlemj  23653  pntlemi  23654  pntlemf  23655  pntlemk  23656  pntlemo  23657  pntleme  23658  pntlem3  23659  pntleml  23661  abvcxp  23665  axtgpasch  23729  cgr3simp2  23777  legso  23850  hlne2  23855  hlln  23856  mirhl  23924  hlperpnel  23964  opphllem4  23987  wlkonwlk  24402  constr3pth  24525  vfwlkniswwlkn  24571  clwwlknscsh  24684  erclwwlknsym  24691  erclwwlkntr  24692  eupaf1o  24835  grpoass  25070  vcsm  25307  nvf  25426  ssps  25508  minvecolem2  25656  minvecolem4c  25660  minvecolem4  25661  minvecolem5  25662  minvecolem6  25663  eigvec1  26746  eliccelico  27453  elicoelioo  27454  slmdvsdi  27624  slmdvs1  27629  cnre2csqlem  27758  lmxrge0  27800  rnlogbval  27882  nnlogbexp  27886  sigaclci  27998  difelsiga  27999  insiga  28003  measvnul  28043  sibfrn  28145  eulerpartlemt  28176  eulerpartlemmf  28180  tg5segofs  28419  subfacp1lem2a  28490  subfacp1lem3  28492  subfacp1lem4  28493  subfacp1lem5  28494  sconpht2  28549  sconpi1  28550  rescon  28557  cvmsss  28578  cvmsn0  28579  cvmlift2lem3  28616  cvmlift2lem7  28620  cvmliftphtlem  28628  cvmliftpht  28629  cvmlift3lem5  28634  cvmlift3lem6  28635  msrf  28768  elmsta  28774  mclsax  28795  mthmpps  28808  mclspps  28810  ghomgrplem  28895  ghomfo  28897  ghomgsg  28899  ibladdnc  30040  iblabsnclem  30046  ftc1cnnclem  30056  ftc1anc  30066  ftc2nc  30067  ivthALT  30121  heiborlem3  30277  iccbnd  30304  rngohom1  30339  idl0cl  30383  maxidlnr  30407  cvgdvgrat  31163  elicore  31469  iccshift  31490  iccsuble  31491  icoiccdif  31496  mullimc  31526  limccog  31530  mullimcf  31533  lptioo2  31541  limcmptdm  31545  limcicciooub  31547  icccncfext  31593  cncfioobdlem  31602  ditgeqiooicc  31645  itgsubsticc  31661  iblcncfioo  31663  itgiccshift  31665  itgperiod  31666  itgsbtaddcnst  31667  stoweidlem11  31678  stoweidlem31  31698  stoweidlem36  31703  stoweidlem38  31705  stoweidlem44  31711  stoweidlem62  31729  dirkercncflem1  31770  dirkercncflem4  31773  fourierdlem26  31800  fourierdlem32  31806  fourierdlem33  31807  fourierdlem37  31811  fourierdlem42  31816  fourierdlem54  31828  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem69  31843  fourierdlem74  31848  fourierdlem75  31849  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem93  31867  fourierdlem101  31875  fourierdlem111  31885  sigardiv  31912  sigarcol  31915  sharhght  31916  sigaradd  31917  cevathlem1  31918  cevathlem2  31919  cevath  31920  lelttrdi  32157  lshpne  34409  opococ  34622  opexmid  34634  hlclat  34785  lclkrslem2  36967