Theorem simp2d 1007

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 995	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 16	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  simp2bi  1010  f1dom3fv3dif  6076  f1dom3el3dif  6077  oeeui  7169  erinxp  7303  resixp  7423  domssex  7597  cantnflem1a  8017  cantnflem1d  8020  cantnflem3  8023  cantnflem4  8024  cantnflem1aOLD  8040  cantnflem1dOLD  8043  cantnflem3OLD  8045  cantnflem4OLD  8046  fpwwe2lem7  8925  canthnumlem  8937  canthp1lem2  8942  wun0  9007  supmullem2  10426  supmul  10427  ixxdisj  11465  ixxun  11466  ixxss1  11468  ixxss2  11469  ixxss12  11470  ixxub  11471  ixxlb  11472  ubioo  11482  iccgelb  11502  iccss2  11516  icodisj  11566  xov1plusxeqvd  11587  fldiv  11887  immul  12971  sqrtge0  13093  sqrtrege0  13200  icco1  13365  ruclem2  13967  ruclem3  13968  ruclem8  13972  ruclem12  13976  gcddvds  14155  crt  14310  phimullem  14311  eulerthlem1  14313  eulerthlem2  14314  prmreclem3  14438  sectcan  15161  sectco  15162  sectmon  15188  monsect  15189  funcixp  15273  funcsect  15278  invfuc  15380  coapm  15467  catciso  15503  posasymb  15699  ipodrsima  15912  pstr2  15952  psdmrn  15954  psref  15955  mhmlin  16090  subm0cl  16100  eqger  16368  eqgcpbl  16372  gaorber  16463  orbstafun  16466  cayleyth  16557  pmtrrn2  16602  pmtrfinv  16603  dfod2  16703  sylow2blem1  16757  dprdf  17152  dprdff  17159  dprdfcl  17160  dprdffOLD  17165  dprdfclOLD  17166  dprdsplit  17210  dpjcntz  17214  ablfac1a  17233  ablfac1b  17234  lmodvsdi  17648  lbssp  17838  2idlcpbl  17995  assaring  18082  mpff  18315  mpfaddcl  18316  mpfmulcl  18317  mpfind  18318  pf1rcl  18498  mpfpf1  18500  mdetunilem2  19200  mdetunilem5  19203  mdetunilem6  19204  chfacfisfcpmat  19441  pnfnei  19807  cnptop2  19830  lmcl  19884  lmcnp  19891  flimfil  20555  tlmlmod  20776  ustbasel  20794  ustincl  20795  ustinvel  20797  ustfilxp  20800  tusunif  20857  imasdsf1olem  20961  xmeter  21021  tmsds  21072  metustexhalfOLD  21151  metustexhalf  21152  nlmlmod  21272  qdensere  21362  blcvx  21388  tgqioo  21390  icccmplem2  21413  reconnlem1  21416  cnmpt2pc  21513  phtpcer  21580  phtpcco2  21584  pcohtpylem  21604  pcohtpy  21605  pcophtb  21614  om1addcl  21618  pi1blem  21624  pi1cpbl  21629  pi1grplem  21634  pi1inv  21637  pi1xfrf  21638  pi1xfr  21640  pi1xfrcnvlem  21641  pi1cof  21644  pi1coghm  21646  cphnlm  21704  cphsqrtcl2  21718  tchcph  21765  lmcau  21836  bcthlem4  21851  minveclem4c  21925  minveclem2  21926  minveclem3b  21928  minveclem4  21932  minveclem6  21934  ivthicc  21955  ovolfsval  21967  ovollb2lem  21984  ovolshftlem1  22005  ovolscalem1  22009  ovolicc1  22012  ovolicc2lem2  22014  ovolicc2lem4  22016  ovolicc2lem5  22017  ovolicopnf  22020  ioombl1lem1  22053  ioombl1lem3  22055  ioombl1lem4  22056  uniioovol  22073  uniioombllem2a  22076  uniioombllem2  22077  uniioombllem3a  22078  uniioombllem3  22079  uniioombllem4  22080  uniioombllem6  22082  dyadmaxlem  22091  volivth  22101  vitalilem2  22103  vitalilem5  22106  i1frn  22169  itg2monolem1  22242  itgcnlem  22281  itgrevallem1  22286  itgreval  22288  itgle  22301  ibladd  22312  iblabslem  22319  itgspliticc  22328  itgsplitioo  22329  ditgcl  22347  ditgswap  22348  ditgsplitlem  22349  limcdif  22365  limcresi  22374  limccnp  22380  limccnp2  22381  limcco  22382  dvlip  22479  dvlip2  22481  dveq0  22486  dvgt0lem1  22488  dvivthlem1  22494  dvcnvrelem1  22503  dvcnvre  22505  dvfsumlem2  22513  ftc1lem1  22521  ftc1a  22523  ftc1lem4  22525  ftc2ditglem  22531  itgsubstlem  22534  ply1rem  22649  fta1glem1  22651  ig1pdvds  22662  plyrem  22786  facth  22787  fta1lem  22788  vieta1lem1  22791  vieta1lem2  22792  aaliou3lem3  22825  aaliou3lem4  22827  aaliou3lem7  22830  taylfvallem1  22837  tayl0  22842  taylply2  22848  radcnvle  22900  psercnlem2  22904  psercnlem1  22905  psercn  22906  pserdvlem1  22907  pserdvlem2  22908  abelth2  22922  coseq00topi  22980  coseq0negpitopi  22981  cosordlem  23003  tanord1  23009  efif1olem1  23014  loglesqrt  23219  logreclem  23220  relogbval  23230  nnlogbexp  23239  chordthmlem4  23282  quart1  23303  quartlem2  23305  quartlem3  23306  quartlem4  23307  quart  23308  acosbnd  23347  atancj  23357  atanlogsublem  23362  atantan  23370  atanbndlem  23372  dvatan  23382  atantayl  23384  rlimcnp2  23413  divsqrtsumlem  23426  ftalem5  23467  ftalem7  23469  basellem4  23474  basellem5  23475  perfectlem2  23622  dchrinv  23653  chpdifbndlem1  23855  pntibndlem2  23893  pntlemc  23897  pntlema  23898  pntlemb  23899  pntlemg  23900  pntlemh  23901  pntlemq  23903  pntlemr  23904  pntlemj  23905  pntlemi  23906  pntlemf  23907  pntlemk  23908  pntlemo  23909  pntleme  23910  pntlem3  23911  pntleml  23913  abvcxp  23917  axtgpasch  23981  cgr3simp2  24032  legso  24105  hlne2  24110  hlln  24111  mirhl  24179  hlperpnel  24219  opphllem4  24242  wlkonwlk  24658  constr3pth  24781  vfwlkniswwlkn  24827  clwwlknscsh  24940  erclwwlknsym  24947  erclwwlkntr  24948  eupaf1o  25091  grpoass  25322  vcsm  25559  nvf  25678  ssps  25760  minvecolem2  25908  minvecolem4c  25912  minvecolem4  25913  minvecolem5  25914  minvecolem6  25915  eigvec1  26997  eliccelico  27741  elicoelioo  27742  slmdvsdi  27911  slmdvs1  27916  cnre2csqlem  28046  lmxrge0  28088  sigaclci  28281  difelsiga  28282  insiga  28286  sigapildsyslem  28306  sigapildsys  28307  measvnul  28333  sibfrn  28462  eulerpartlemt  28493  eulerpartlemmf  28497  tg5segofs  28736  subfacp1lem2a  28813  subfacp1lem3  28815  subfacp1lem4  28816  subfacp1lem5  28817  sconpht2  28872  sconpi1  28873  rescon  28880  cvmsss  28901  cvmsn0  28902  cvmlift2lem3  28939  cvmlift2lem7  28943  cvmliftphtlem  28951  cvmliftpht  28952  cvmlift3lem5  28957  cvmlift3lem6  28958  msrf  29091  elmsta  29097  mclsax  29118  mthmpps  29131  mclspps  29133  ghomgrplem  29218  ghomfo  29220  ghomgsg  29222  ibladdnc  30238  iblabsnclem  30244  ftc1cnnclem  30254  ftc1anc  30264  ftc2nc  30265  ivthALT  30319  heiborlem3  30475  iccbnd  30502  rngohom1  30537  idl0cl  30581  maxidlnr  30605  cvgdvgrat  31362  elicore  31703  iccshift  31724  iccsuble  31725  icoiccdif  31730  mullimc  31788  limccog  31792  mullimcf  31795  lptioo2  31803  limcmptdm  31807  limcicciooub  31809  icccncfext  31856  cncfioobdlem  31865  ditgeqiooicc  31925  itgsubsticc  31941  iblcncfioo  31943  itgiccshift  31945  itgperiod  31946  itgsbtaddcnst  31947  stoweidlem11  31959  stoweidlem31  31979  stoweidlem36  31984  stoweidlem38  31986  stoweidlem44  31992  stoweidlem62  32010  dirkercncflem1  32051  dirkercncflem4  32054  fourierdlem26  32081  fourierdlem32  32087  fourierdlem33  32088  fourierdlem37  32092  fourierdlem42  32097  fourierdlem54  32109  fourierdlem63  32118  fourierdlem64  32119  fourierdlem65  32120  fourierdlem69  32124  fourierdlem74  32129  fourierdlem75  32130  fourierdlem79  32134  fourierdlem81  32136  fourierdlem82  32137  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem93  32148  fourierdlem101  32156  fourierdlem111  32166  sigardiv  32244  sigarcol  32247  sharhght  32248  sigaradd  32249  cevathlem1  32250  cevathlem2  32251  cevath  32252  perfectALTVlem2  32544  proththd  32548  lelttrdi  32644  lshpne  35120  opococ  35333  opexmid  35345  hlclat  35496  lclkrslem2  37678