Theorem simp2d 970

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

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  simp2bi  973  oeeui  6804  erinxp  6937  resixp  7056  domssex  7227  cantnflem1a  7597  cantnflem1d  7600  cantnflem3  7603  cantnflem4  7604  fpwwe2lem7  8467  canthnumlem  8479  canthp1lem2  8484  wun0  8549  supmullem2  9931  supmul  9932  ixxdisj  10887  ixxun  10888  ixxss1  10890  ixxss2  10891  ixxss12  10892  ixxub  10893  ixxlb  10894  ubioo  10904  iccss2  10937  icodisj  10978  xov1plusxeqvd  10997  fldiv  11196  immul  11896  sqrge0  12018  sqrrege0  12124  icco1  12289  ruclem2  12786  ruclem3  12787  ruclem8  12791  ruclem12  12795  gcddvds  12970  crt  13122  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  prmreclem3  13241  sectcan  13936  sectco  13937  sectmon  13958  monsect  13959  funcixp  14019  funcsect  14024  invfuc  14126  coapm  14181  catciso  14217  posasymb  14364  ipodrsima  14546  pstr2  14592  psdmrn  14594  psref  14595  mhmlin  14700  subm0cl  14707  eqger  14945  eqgcpbl  14949  gaorber  15040  orbstafun  15043  cayleyth  15068  dfod2  15155  sylow2blem1  15209  dprdf  15519  dprdff  15525  dprdfcl  15526  dprdsplit  15561  dpjcntz  15565  ablfac1a  15582  ablfac1b  15583  lmodvsdi  15928  lbssp  16106  2idlcpbl  16260  assarng  16335  pnfnei  17238  cnptop2  17261  lmcl  17315  lmcnp  17322  flimfil  17954  tlmlmod  18171  ustbasel  18189  ustincl  18190  ustinvel  18192  ustfilxp  18195  tusunif  18252  imasdsf1olem  18356  xmeter  18416  tmsds  18467  metustexhalfOLD  18546  metustexhalf  18547  nlmlmod  18667  qdensere  18757  blcvx  18782  tgqioo  18784  icccmplem2  18807  reconnlem1  18810  cnmpt2pc  18906  phtpcer  18973  phtpcco2  18977  pcohtpylem  18997  pcohtpy  18998  pcophtb  19007  om1addcl  19011  pi1blem  19017  pi1cpbl  19022  pi1grplem  19027  pi1inv  19030  pi1xfrf  19031  pi1xfr  19033  pi1xfrcnvlem  19034  pi1cof  19037  pi1coghm  19039  cphnlm  19088  cphsqrcl2  19102  tchcph  19147  lmcau  19218  bcthlem4  19233  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  ivthicc  19308  ovolfsval  19320  ovollb2lem  19337  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem2  19367  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicopnf  19373  ioombl1lem1  19405  ioombl1lem3  19407  ioombl1lem4  19408  uniioovol  19424  uniioombllem2a  19427  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  dyadmaxlem  19442  volivth  19452  vitalilem2  19454  vitalilem5  19457  i1frn  19522  itg2monolem1  19595  itgcnlem  19634  itgrevallem1  19639  itgreval  19641  itgle  19654  ibladd  19665  iblabslem  19672  itgspliticc  19681  itgsplitioo  19682  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  limcdif  19716  limcresi  19725  limccnp  19731  limccnp2  19732  limcco  19733  dvlip  19830  dvlip2  19832  dveq0  19837  dvgt0lem1  19839  dvivthlem1  19845  dvcnvrelem1  19854  dvcnvre  19856  dvfsumlem2  19864  ftc1lem1  19872  ftc1a  19874  ftc1lem4  19876  ftc2ditglem  19882  itgsubstlem  19885  mpff  19915  mpfaddcl  19916  mpfmulcl  19917  mpfind  19918  pf1rcl  19922  mpfpf1  19924  ply1rem  20039  fta1glem1  20041  ig1pdvds  20052  plyrem  20175  facth  20176  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  aaliou3lem3  20214  aaliou3lem4  20216  aaliou3lem7  20219  taylfvallem1  20226  tayl0  20231  taylply2  20237  radcnvle  20289  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  abelth2  20311  coseq00topi  20363  coseq0negpitopi  20364  cosordlem  20386  tanord1  20392  efif1olem1  20397  loglesqr  20595  logreclem  20613  chordthmlem4  20629  quart1  20649  quartlem2  20651  quartlem3  20652  quartlem4  20653  quart  20654  acosbnd  20693  atancj  20703  atanlogsublem  20708  atantan  20716  atanbndlem  20718  dvatan  20728  atantayl  20730  rlimcnp2  20758  divsqrsumlem  20771  ftalem5  20812  ftalem7  20814  basellem4  20819  basellem5  20820  perfectlem2  20967  dchrinv  20998  chpdifbndlem1  21200  pntibndlem2  21238  pntlemc  21242  pntlema  21243  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemi  21251  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntleme  21255  pntlem3  21256  pntleml  21258  abvcxp  21262  wlkonwlk  21488  constr3pth  21600  eupaf1o  21645  grpoass  21744  vcsm  21981  nvf  22100  ssps  22182  minvecolem2  22330  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  eigvec1  23418  iccgelb  24089  eliccelico  24093  elicoelioo  24094  cnre2csqlem  24261  lmxrge0  24290  rnlogbval  24353  nnlogbexp  24357  sigaclci  24468  difelsiga  24469  insiga  24473  measvnul  24513  sibfrn  24605  subfacp1lem2a  24819  subfacp1lem3  24821  subfacp1lem4  24822  subfacp1lem5  24823  sconpht2  24878  sconpi1  24879  rescon  24886  cvmsss  24907  cvmsn0  24908  cvmlift2lem3  24945  cvmlift2lem7  24949  cvmliftphtlem  24957  cvmliftpht  24958  cvmlift3lem5  24963  cvmlift3lem6  24964  ghomgrplem  25053  ghomfo  25055  ghomgsg  25057  ibladdnc  26161  iblabsnclem  26167  ftc1cnnclem  26177  ivthALT  26228  heiborlem3  26412  iccbnd  26439  rngohom1  26474  idl0cl  26518  maxidlnr  26542  pmtrfinv  27270  stoweidlem11  27627  stoweidlem31  27647  stoweidlem36  27652  stoweidlem38  27654  stoweidlem44  27660  stoweidlem62  27678  sigardiv  27718  sigarcol  27721  sharhght  27722  sigaradd  27723  cevathlem1  27724  cevathlem2  27725  cevath  27726  lshpne  29465  opococ  29678  opexmid  29690  hlclat  29841  lclkrslem2  32021

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