Theorem simp2d 1004

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  simp2bi  1007  f1dom3fv3dif  6154  f1dom3el3dif  6155  oeeui  7241  erinxp  7375  resixp  7494  domssex  7668  cantnflem1a  8093  cantnflem1d  8096  cantnflem3  8099  cantnflem4  8100  cantnflem1aOLD  8116  cantnflem1dOLD  8119  cantnflem3OLD  8121  cantnflem4OLD  8122  fpwwe2lem7  9003  canthnumlem  9015  canthp1lem2  9020  wun0  9085  supmullem2  10499  supmul  10500  ixxdisj  11533  ixxun  11534  ixxss1  11536  ixxss2  11537  ixxss12  11538  ixxub  11539  ixxlb  11540  ubioo  11550  iccgelb  11570  iccss2  11584  icodisj  11634  xov1plusxeqvd  11655  fldiv  11943  immul  12919  sqrge0  13041  sqrrege0  13147  icco1  13312  ruclem2  13815  ruclem3  13816  ruclem8  13820  ruclem12  13824  gcddvds  14001  crt  14156  phimullem  14157  eulerthlem1  14159  eulerthlem2  14160  prmreclem3  14284  sectcan  15000  sectco  15001  sectmon  15022  monsect  15023  funcixp  15083  funcsect  15088  invfuc  15190  coapm  15245  catciso  15281  posasymb  15428  ipodrsima  15641  pstr2  15681  psdmrn  15683  psref  15684  mhmlin  15777  subm0cl  15786  eqger  16039  eqgcpbl  16043  gaorber  16134  orbstafun  16137  cayleyth  16228  pmtrrn2  16274  pmtrfinv  16275  dfod2  16375  sylow2blem1  16429  dprdf  16823  dprdff  16829  dprdfcl  16830  dprdffOLD  16835  dprdfclOLD  16836  dprdsplit  16880  dpjcntz  16884  ablfac1a  16903  ablfac1b  16904  rngsrg  17017  lmodvsdi  17311  lbssp  17501  2idlcpbl  17657  assarng  17733  mpff  17966  mpfaddcl  17967  mpfmulcl  17968  mpfind  17969  pf1rcl  18149  mpfpf1  18151  mdetunilem2  18875  mdetunilem5  18878  mdetunilem6  18879  chfacfisfcpmat  19116  pnfnei  19480  cnptop2  19503  lmcl  19557  lmcnp  19564  flimfil  20198  tlmlmod  20419  ustbasel  20437  ustincl  20438  ustinvel  20440  ustfilxp  20443  tusunif  20500  imasdsf1olem  20604  xmeter  20664  tmsds  20715  metustexhalfOLD  20794  metustexhalf  20795  nlmlmod  20915  qdensere  21005  blcvx  21031  tgqioo  21033  icccmplem2  21056  reconnlem1  21059  cnmpt2pc  21156  phtpcer  21223  phtpcco2  21227  pcohtpylem  21247  pcohtpy  21248  pcophtb  21257  om1addcl  21261  pi1blem  21267  pi1cpbl  21272  pi1grplem  21277  pi1inv  21280  pi1xfrf  21281  pi1xfr  21283  pi1xfrcnvlem  21284  pi1cof  21287  pi1coghm  21289  cphnlm  21347  cphsqrcl2  21361  tchcph  21408  lmcau  21479  bcthlem4  21494  minveclem4c  21568  minveclem2  21569  minveclem3b  21571  minveclem4  21575  minveclem6  21577  ivthicc  21598  ovolfsval  21610  ovollb2lem  21627  ovolshftlem1  21648  ovolscalem1  21652  ovolicc1  21655  ovolicc2lem2  21657  ovolicc2lem4  21659  ovolicc2lem5  21660  ovolicopnf  21663  ioombl1lem1  21696  ioombl1lem3  21698  ioombl1lem4  21699  uniioovol  21716  uniioombllem2a  21719  uniioombllem2  21720  uniioombllem3a  21721  uniioombllem3  21722  uniioombllem4  21723  uniioombllem6  21725  dyadmaxlem  21734  volivth  21744  vitalilem2  21746  vitalilem5  21749  i1frn  21812  itg2monolem1  21885  itgcnlem  21924  itgrevallem1  21929  itgreval  21931  itgle  21944  ibladd  21955  iblabslem  21962  itgspliticc  21971  itgsplitioo  21972  ditgcl  21990  ditgswap  21991  ditgsplitlem  21992  limcdif  22008  limcresi  22017  limccnp  22023  limccnp2  22024  limcco  22025  dvlip  22122  dvlip2  22124  dveq0  22129  dvgt0lem1  22131  dvivthlem1  22137  dvcnvrelem1  22146  dvcnvre  22148  dvfsumlem2  22156  ftc1lem1  22164  ftc1a  22166  ftc1lem4  22168  ftc2ditglem  22174  itgsubstlem  22177  ply1rem  22292  fta1glem1  22294  ig1pdvds  22305  plyrem  22428  facth  22429  fta1lem  22430  vieta1lem1  22433  vieta1lem2  22434  aaliou3lem3  22467  aaliou3lem4  22469  aaliou3lem7  22472  taylfvallem1  22479  tayl0  22484  taylply2  22490  radcnvle  22542  psercnlem2  22546  psercnlem1  22547  psercn  22548  pserdvlem1  22549  pserdvlem2  22550  abelth2  22564  coseq00topi  22621  coseq0negpitopi  22622  cosordlem  22644  tanord1  22650  efif1olem1  22655  loglesqr  22853  logreclem  22871  chordthmlem4  22887  quart1  22908  quartlem2  22910  quartlem3  22911  quartlem4  22912  quart  22913  acosbnd  22952  atancj  22962  atanlogsublem  22967  atantan  22975  atanbndlem  22977  dvatan  22987  atantayl  22989  rlimcnp2  23017  divsqrsumlem  23030  ftalem5  23071  ftalem7  23073  basellem4  23078  basellem5  23079  perfectlem2  23226  dchrinv  23257  chpdifbndlem1  23459  pntibndlem2  23497  pntlemc  23501  pntlema  23502  pntlemb  23503  pntlemg  23504  pntlemh  23505  pntlemq  23507  pntlemr  23508  pntlemj  23509  pntlemi  23510  pntlemf  23511  pntlemk  23512  pntlemo  23513  pntleme  23514  pntlem3  23515  pntleml  23517  abvcxp  23521  axtgpasch  23585  cgr3simp2  23633  legso  23705  colline  23736  wlkonwlk  24199  constr3pth  24322  vfwlkniswwlkn  24368  clwwlknscsh  24481  erclwwlknsym  24488  erclwwlkntr  24489  eupaf1o  24632  grpoass  24731  vcsm  24968  nvf  25087  ssps  25169  minvecolem2  25317  minvecolem4c  25321  minvecolem4  25322  minvecolem5  25323  minvecolem6  25324  eigvec1  26407  eliccelico  27106  elicoelioo  27107  ogrpaddlt  27220  slmdvsdi  27270  slmdvs1  27275  cnre2csqlem  27378  lmxrge0  27420  rnlogbval  27506  nnlogbexp  27510  sigaclci  27622  difelsiga  27623  insiga  27627  measvnul  27667  sibfrn  27769  eulerpartlemt  27800  eulerpartlemmf  27804  tg5segofs  28043  subfacp1lem2a  28114  subfacp1lem3  28116  subfacp1lem4  28117  subfacp1lem5  28118  sconpht2  28173  sconpi1  28174  rescon  28181  cvmsss  28202  cvmsn0  28203  cvmlift2lem3  28240  cvmlift2lem7  28244  cvmliftphtlem  28252  cvmliftpht  28253  cvmlift3lem5  28258  cvmlift3lem6  28259  ghomgrplem  28354  ghomfo  28356  ghomgsg  28358  ibladdnc  29500  iblabsnclem  29506  ftc1cnnclem  29516  ftc1anc  29526  ftc2nc  29527  ivthALT  29581  heiborlem3  29763  iccbnd  29790  rngohom1  29825  idl0cl  29869  maxidlnr  29893  elicore  30920  iccshift  30941  iccsuble  30942  icoiccdif  30947  mullimc  30977  limccog  30981  mullimcf  30984  lptioo2  30992  limcmptdm  30996  limcicciooub  30998  icccncfext  31045  cncfiooicclem1  31051  cncfioobdlem  31054  ditgeqiooicc  31097  itgsubsticc  31113  iblcncfioo  31115  itgiccshift  31117  itgperiod  31118  itgsbtaddcnst  31119  stoweidlem11  31130  stoweidlem31  31150  stoweidlem36  31155  stoweidlem38  31157  stoweidlem44  31163  stoweidlem62  31181  dirkercncflem1  31222  dirkercncflem4  31225  fourierdlem26  31252  fourierdlem27  31253  fourierdlem32  31258  fourierdlem33  31259  fourierdlem37  31263  fourierdlem42  31268  fourierdlem54  31280  fourierdlem63  31289  fourierdlem64  31290  fourierdlem65  31291  fourierdlem69  31295  fourierdlem74  31300  fourierdlem75  31301  fourierdlem79  31305  fourierdlem81  31307  fourierdlem82  31308  fourierdlem89  31315  fourierdlem90  31316  fourierdlem91  31317  fourierdlem93  31319  fourierdlem101  31327  fourierdlem111  31337  sigardiv  31364  sigarcol  31367  sharhght  31368  sigaradd  31369  cevathlem1  31370  cevathlem2  31371  cevath  31372  lelttrdi  31611  lshpne  33654  opococ  33867  opexmid  33879  hlclat  34030  lclkrslem2  36210