Theorem simp2d 1001

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

Syntax hints:   -> wi 4   /\ w3a 965

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 967

This theorem is referenced by:  simp2bi  1004  f1dom3fv3dif  6079  f1dom3el3dif  6080  oeeui  7141  erinxp  7274  resixp  7398  domssex  7572  cantnflem1a  7994  cantnflem1d  7997  cantnflem3  8000  cantnflem4  8001  cantnflem1aOLD  8017  cantnflem1dOLD  8020  cantnflem3OLD  8022  cantnflem4OLD  8023  fpwwe2lem7  8904  canthnumlem  8916  canthp1lem2  8921  wun0  8986  supmullem2  10398  supmul  10399  ixxdisj  11416  ixxun  11417  ixxss1  11419  ixxss2  11420  ixxss12  11421  ixxub  11422  ixxlb  11423  ubioo  11433  iccgelb  11453  iccss2  11467  icodisj  11511  xov1plusxeqvd  11532  fldiv  11800  immul  12727  sqrge0  12849  sqrrege0  12955  icco1  13120  ruclem2  13616  ruclem3  13617  ruclem8  13621  ruclem12  13625  gcddvds  13801  crt  13955  phimullem  13956  eulerthlem1  13958  eulerthlem2  13959  prmreclem3  14081  sectcan  14796  sectco  14797  sectmon  14818  monsect  14819  funcixp  14879  funcsect  14884  invfuc  14986  coapm  15041  catciso  15077  posasymb  15224  ipodrsima  15437  pstr2  15477  psdmrn  15479  psref  15480  mhmlin  15573  subm0cl  15582  eqger  15833  eqgcpbl  15837  gaorber  15928  orbstafun  15931  cayleyth  16022  pmtrrn2  16068  pmtrfinv  16069  dfod2  16169  sylow2blem1  16223  dprdf  16595  dprdff  16601  dprdfcl  16602  dprdffOLD  16607  dprdfclOLD  16608  dprdsplit  16652  dpjcntz  16656  ablfac1a  16675  ablfac1b  16676  rngsrg  16789  lmodvsdi  17077  lbssp  17266  2idlcpbl  17422  assarng  17498  mpff  17726  mpfaddcl  17727  mpfmulcl  17728  mpfind  17729  pf1rcl  17892  mpfpf1  17894  mdetunilem2  18535  mdetunilem5  18538  mdetunilem6  18539  pnfnei  18940  cnptop2  18963  lmcl  19017  lmcnp  19024  flimfil  19658  tlmlmod  19879  ustbasel  19897  ustincl  19898  ustinvel  19900  ustfilxp  19903  tusunif  19960  imasdsf1olem  20064  xmeter  20124  tmsds  20175  metustexhalfOLD  20254  metustexhalf  20255  nlmlmod  20375  qdensere  20465  blcvx  20491  tgqioo  20493  icccmplem2  20516  reconnlem1  20519  cnmpt2pc  20616  phtpcer  20683  phtpcco2  20687  pcohtpylem  20707  pcohtpy  20708  pcophtb  20717  om1addcl  20721  pi1blem  20727  pi1cpbl  20732  pi1grplem  20737  pi1inv  20740  pi1xfrf  20741  pi1xfr  20743  pi1xfrcnvlem  20744  pi1cof  20747  pi1coghm  20749  cphnlm  20807  cphsqrcl2  20821  tchcph  20868  lmcau  20939  bcthlem4  20954  minveclem4c  21028  minveclem2  21029  minveclem3b  21031  minveclem4  21035  minveclem6  21037  ivthicc  21058  ovolfsval  21070  ovollb2lem  21087  ovolshftlem1  21108  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem2  21117  ovolicc2lem4  21119  ovolicc2lem5  21120  ovolicopnf  21123  ioombl1lem1  21155  ioombl1lem3  21157  ioombl1lem4  21158  uniioovol  21175  uniioombllem2a  21178  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem6  21184  dyadmaxlem  21193  volivth  21203  vitalilem2  21205  vitalilem5  21208  i1frn  21271  itg2monolem1  21344  itgcnlem  21383  itgrevallem1  21388  itgreval  21390  itgle  21403  ibladd  21414  iblabslem  21421  itgspliticc  21430  itgsplitioo  21431  ditgcl  21449  ditgswap  21450  ditgsplitlem  21451  limcdif  21467  limcresi  21476  limccnp  21482  limccnp2  21483  limcco  21484  dvlip  21581  dvlip2  21583  dveq0  21588  dvgt0lem1  21590  dvivthlem1  21596  dvcnvrelem1  21605  dvcnvre  21607  dvfsumlem2  21615  ftc1lem1  21623  ftc1a  21625  ftc1lem4  21627  ftc2ditglem  21633  itgsubstlem  21636  ply1rem  21751  fta1glem1  21753  ig1pdvds  21764  plyrem  21887  facth  21888  fta1lem  21889  vieta1lem1  21892  vieta1lem2  21893  aaliou3lem3  21926  aaliou3lem4  21928  aaliou3lem7  21931  taylfvallem1  21938  tayl0  21943  taylply2  21949  radcnvle  22001  psercnlem2  22005  psercnlem1  22006  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  abelth2  22023  coseq00topi  22080  coseq0negpitopi  22081  cosordlem  22103  tanord1  22109  efif1olem1  22114  loglesqr  22312  logreclem  22330  chordthmlem4  22346  quart1  22367  quartlem2  22369  quartlem3  22370  quartlem4  22371  quart  22372  acosbnd  22411  atancj  22421  atanlogsublem  22426  atantan  22434  atanbndlem  22436  dvatan  22446  atantayl  22448  rlimcnp2  22476  divsqrsumlem  22489  ftalem5  22530  ftalem7  22532  basellem4  22537  basellem5  22538  perfectlem2  22685  dchrinv  22716  chpdifbndlem1  22918  pntibndlem2  22956  pntlemc  22960  pntlema  22961  pntlemb  22962  pntlemg  22963  pntlemh  22964  pntlemq  22966  pntlemr  22967  pntlemj  22968  pntlemi  22969  pntlemf  22970  pntlemk  22971  pntlemo  22972  pntleme  22973  pntlem3  22974  pntleml  22976  abvcxp  22980  axtgpasch  23044  cgr3simp2  23092  colline  23177  wlkonwlk  23569  constr3pth  23681  eupaf1o  23726  grpoass  23825  vcsm  24062  nvf  24181  ssps  24263  minvecolem2  24411  minvecolem4c  24415  minvecolem4  24416  minvecolem5  24417  minvecolem6  24418  eigvec1  25501  eliccelico  26201  elicoelioo  26202  ogrpaddlt  26315  slmdvsdi  26365  slmdvs1  26370  cnre2csqlem  26474  lmxrge0  26516  rnlogbval  26593  nnlogbexp  26597  sigaclci  26709  difelsiga  26710  insiga  26714  measvnul  26754  sibfrn  26857  eulerpartlemt  26888  eulerpartlemmf  26892  tg5segofs  27131  subfacp1lem2a  27202  subfacp1lem3  27204  subfacp1lem4  27205  subfacp1lem5  27206  sconpht2  27261  sconpi1  27262  rescon  27269  cvmsss  27290  cvmsn0  27291  cvmlift2lem3  27328  cvmlift2lem7  27332  cvmliftphtlem  27340  cvmliftpht  27341  cvmlift3lem5  27346  cvmlift3lem6  27347  ghomgrplem  27442  ghomfo  27444  ghomgsg  27446  ibladdnc  28587  iblabsnclem  28593  ftc1cnnclem  28603  ftc1anc  28613  ftc2nc  28614  ivthALT  28668  heiborlem3  28850  iccbnd  28877  rngohom1  28912  idl0cl  28956  maxidlnr  28980  stoweidlem11  29944  stoweidlem31  29964  stoweidlem36  29969  stoweidlem38  29971  stoweidlem44  29977  stoweidlem62  29995  sigardiv  30035  sigarcol  30038  sharhght  30039  sigaradd  30040  cevathlem1  30041  cevathlem2  30042  cevath  30043  lelttrdi  30316  vfwlkniswwlkn  30478  Lemma2  30631  erclwwlknsym  30638  erclwwlkntr  30639  chfacfisfcpmat  31309  lshpne  32933  opococ  33146  opexmid  33158  hlclat  33309  lclkrslem2  35489