Theorem simp2d 1022

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

Syntax hints:   -> wi 4   /\ w3a 986

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 190  df-an 377  df-3an 988

This theorem is referenced by:  simp2bi  1025  f1dom3fv3dif  6154  f1dom3el3dif  6155  f1prex  6168  oeeui  7290  erinxp  7424  resixp  7544  domssex  7720  cantnflem1a  8177  cantnflem1d  8180  cantnflem3  8183  cantnflem4  8184  fpwwe2lem7  9048  canthnumlem  9060  canthp1lem2  9065  wun0  9130  supmullem2  10567  supmul  10568  ixxdisj  11640  ixxun  11641  ixxss1  11643  ixxss2  11644  ixxss12  11645  ixxub  11646  ixxlb  11647  ixxlbOLD  11648  ubioo  11658  elicore  11677  iccgelb  11681  iccss2  11695  icodisj  11748  xov1plusxeqvd  11769  fldiv  12081  immul  13210  sqrtge0  13332  sqrtrege0  13439  icco1  13615  ruclem2  14295  ruclem3  14296  ruclem8  14300  ruclem12  14304  gcddvds  14488  crt  14737  phimullem  14738  eulerthlem1  14740  eulerthlem2  14741  prmreclem3  14873  sectcan  15671  sectco  15672  sectmon  15698  monsect  15699  funcixp  15783  funcsect  15788  invfuc  15890  coapm  15977  catciso  16013  posasymb  16209  ipodrsima  16422  pstr2  16462  psdmrn  16464  psref  16465  mhmlin  16600  subm0cl  16610  eqger  16878  eqgcpbl  16882  gaorber  16973  orbstafun  16976  cayleyth  17067  pmtrrn2  17112  pmtrfinv  17113  dfod2  17226  sylow2blem1  17283  dprdf  17649  dprdff  17656  dprdfcl  17657  dprdsplit  17692  dpjcntz  17696  ablfac1a  17713  ablfac1b  17714  lmodvsdi  18125  lbssp  18313  2idlcpbl  18469  assaring  18555  mpff  18767  mpfaddcl  18768  mpfmulcl  18769  mpfind  18770  pf1rcl  18948  mpfpf1  18950  mdetunilem2  19649  mdetunilem5  19652  mdetunilem6  19653  chfacfisfcpmat  19890  pnfnei  20247  cnptop2  20270  lmcl  20324  lmcnp  20331  flimfil  20995  tlmlmod  21214  ustbasel  21232  ustincl  21233  ustinvel  21235  ustfilxp  21238  tusunif  21295  imasdsf1olem  21399  xmeter  21459  tmsds  21510  metustexhalf  21582  nlmlmod  21692  qdensere  21801  blcvx  21827  tgqioo  21829  icccmplem2  21852  reconnlem1  21855  cnmpt2pc  21967  phtpcer  22037  phtpcco2  22041  pcohtpylem  22061  pcohtpy  22062  pcophtb  22071  om1addcl  22075  pi1blem  22081  pi1cpbl  22086  pi1grplem  22091  pi1inv  22094  pi1xfrf  22095  pi1xfr  22097  pi1xfrcnvlem  22098  pi1cof  22101  pi1coghm  22103  cphnlm  22161  cphsqrtcl2  22175  tchcph  22222  lmcau  22293  bcthlem4  22306  minveclem4c  22378  minveclem2  22379  minveclem3b  22381  minveclem4  22385  minveclem6  22387  minveclem4cOLD  22390  minveclem2OLD  22391  minveclem3bOLD  22393  minveclem4OLD  22397  minveclem6OLD  22399  ivthicc  22420  ovolfsval  22434  ovollb2lem  22452  ovolshftlem1  22473  ovolscalem1  22477  ovolicc1  22480  ovolicc2lem2  22482  ovolicc2lem4OLD  22484  ovolicc2lem4  22485  ovolicc2lem5  22486  ovolicopnf  22489  ioombl1lem1  22523  ioombl1lem3  22525  ioombl1lem4  22526  uniioovol  22548  uniioombllem2a  22551  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem3a  22554  uniioombllem3  22555  uniioombllem4  22556  uniioombllem6  22558  dyadmaxlem  22567  volivth  22577  vitalilem2  22579  vitalilem5  22582  i1frn  22647  itg2monolem1  22720  itgcnlem  22759  itgrevallem1  22764  itgreval  22766  itgle  22779  ibladd  22790  iblabslem  22797  itgspliticc  22806  itgsplitioo  22807  ditgcl  22825  ditgswap  22826  ditgsplitlem  22827  limcdif  22843  limcresi  22852  limccnp  22858  limccnp2  22859  limcco  22860  dvlip  22957  dvlip2  22959  dveq0  22964  dvgt0lem1  22966  dvivthlem1  22972  dvcnvrelem1  22981  dvcnvre  22983  dvfsumlem2  22991  ftc1lem1  22999  ftc1a  23001  ftc1lem4  23003  ftc2ditglem  23009  itgsubstlem  23012  ply1rem  23126  fta1glem1  23128  ig1pdvds  23140  ig1pdvdsOLD  23146  plyrem  23270  facth  23271  fta1lem  23272  vieta1lem1  23275  vieta1lem2  23276  aaliou3lem3  23312  aaliou3lem4  23314  aaliou3lem7  23317  taylfvallem1  23324  tayl0  23329  taylply2  23335  radcnvle  23387  psercnlem2  23391  psercnlem1  23392  psercn  23393  pserdvlem1  23394  pserdvlem2  23395  abelth2  23409  coseq00topi  23469  coseq0negpitopi  23470  cosordlem  23492  tanord1  23498  efif1olem1  23503  loglesqrt  23710  logreclem  23711  relogbval  23721  nnlogbexp  23730  chordthmlem4  23773  quart1  23794  quartlem2  23796  quartlem3  23797  quartlem4  23798  quart  23799  acosbnd  23838  atancj  23848  atanlogsublem  23853  atantan  23861  atanbndlem  23863  dvatan  23873  atantayl  23875  rlimcnp2  23904  divsqrtsumlem  23917  ftalem5  24013  ftalem5OLD  24015  ftalem7  24017  basellem4  24022  basellem5  24023  perfectlem2  24170  dchrinv  24201  chpdifbndlem1  24403  pntibndlem2  24441  pntlemc  24445  pntlema  24446  pntlemb  24447  pntlemg  24448  pntlemh  24449  pntlemq  24451  pntlemr  24452  pntlemj  24453  pntlemi  24454  pntlemf  24455  pntlemk  24456  pntlemo  24457  pntleme  24458  pntlem3  24459  pntleml  24461  abvcxp  24465  axtgpasch  24527  cgr3simp2  24578  legso  24656  hlne2  24663  hlln  24664  mirhl  24736  hlperpnel  24779  opphllem4  24804  inagswap  24892  wlkonwlk  25277  constr3pth  25400  vfwlkniswwlkn  25446  clwwlknscsh  25559  erclwwlknsym  25566  erclwwlkntr  25567  eupaf1o  25710  grpoass  25943  vcsm  26180  nvf  26299  ssps  26381  minvecolem2  26529  minvecolem4c  26533  minvecolem4  26534  minvecolem5  26535  minvecolem6  26536  minvecolem2OLD  26539  minvecolem4cOLD  26543  minvecolem4OLD  26544  minvecolem5OLD  26545  minvecolem6OLD  26546  eigvec1  27627  eliccelico  28367  elicoelioo  28368  slmdvsdi  28538  slmdvs1  28543  pmtrto1cl  28619  cnre2csqlem  28723  lmxrge0  28765  sigaclci  28961  difelsiga  28962  insiga  28966  ldsysgenld  28989  sigapildsyslem  28990  sigapildsys  28991  ldgenpisyslem1  28992  measvnul  29035  sibfrn  29176  eulerpartlemt  29210  eulerpartlemmf  29214  tg5segofs  29496  subfacp1lem2a  29909  subfacp1lem3  29911  subfacp1lem4  29912  subfacp1lem5  29913  sconpht2  29967  sconpi1  29968  rescon  29975  cvmsss  29996  cvmsn0  29997  cvmlift2lem3  30034  cvmlift2lem7  30038  cvmliftphtlem  30046  cvmliftpht  30047  cvmlift3lem5  30052  cvmlift3lem6  30053  msrf  30186  elmsta  30192  mclsax  30213  mthmpps  30226  mclspps  30228  ghomgrplem  30313  ghomfo  30315  ghomgsg  30317  ivthALT  30997  poimirlem17  31959  poimirlem20  31962  ibladdnc  32001  iblabsnclem  32007  ftc1cnnclem  32017  ftc1anc  32027  ftc2nc  32028  heiborlem3  32147  iccbnd  32174  rngohom1  32209  idl0cl  32253  maxidlnr  32277  lshpne  32550  opococ  32763  opexmid  32775  hlclat  32926  lclkrslem2  35108  cvgdvgrat  36663  iccshift  37660  iccsuble  37661  icoiccdif  37666  mullimc  37738  limccog  37742  mullimcf  37745  lptioo2  37753  limcmptdm  37757  limcicciooub  37759  icccncfext  37807  cncfioobdlem  37816  ditgeqiooicc  37879  itgsubsticc  37895  iblcncfioo  37897  itgiccshift  37899  itgperiod  37900  itgsbtaddcnst  37901  stoweidlem11  37928  stoweidlem31  37949  stoweidlem36  37954  stoweidlem38  37956  stoweidlem44  37962  stoweidlem62  37980  stoweidlem62OLD  37981  dirkercncflem1  38022  dirkercncflem4  38025  fourierdlem26  38052  fourierdlem32  38059  fourierdlem33  38060  fourierdlem37  38064  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem54  38081  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem69  38096  fourierdlem74  38101  fourierdlem75  38102  fourierdlem79  38106  fourierdlem81  38108  fourierdlem82  38109  fourierdlem89  38116  fourierdlem90  38117  fourierdlem91  38118  fourierdlem93  38120  fourierdlem101  38128  fourierdlem111  38138  saldifcl  38237  hoidmv1lelem3  38478  sigardiv  38561  sigarcol  38564  sharhght  38565  sigaradd  38566  cevathlem1  38567  cevathlem2  38568  cevath  38569  perfectALTVlem2  38935  proththd  39005  lelttrdi  39141  subumgredg2  39459  upgrres1  39482  nb3grprlem1  39556  21wlkdlem6  39932