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  5975  f1dom3el3dif  5976  oeeui  7033  erinxp  7166  resixp  7290  domssex  7464  cantnflem1a  7885  cantnflem1d  7888  cantnflem3  7891  cantnflem4  7892  cantnflem1aOLD  7908  cantnflem1dOLD  7911  cantnflem3OLD  7913  cantnflem4OLD  7914  fpwwe2lem7  8795  canthnumlem  8807  canthp1lem2  8812  wun0  8877  supmullem2  10289  supmul  10290  ixxdisj  11307  ixxun  11308  ixxss1  11310  ixxss2  11311  ixxss12  11312  ixxub  11313  ixxlb  11314  ubioo  11324  iccgelb  11344  iccss2  11358  icodisj  11402  xov1plusxeqvd  11423  fldiv  11691  immul  12617  sqrge0  12739  sqrrege0  12845  icco1  13010  ruclem2  13506  ruclem3  13507  ruclem8  13511  ruclem12  13515  gcddvds  13691  crt  13845  phimullem  13846  eulerthlem1  13848  eulerthlem2  13849  prmreclem3  13971  sectcan  14686  sectco  14687  sectmon  14708  monsect  14709  funcixp  14769  funcsect  14774  invfuc  14876  coapm  14931  catciso  14967  posasymb  15114  ipodrsima  15327  pstr2  15367  psdmrn  15369  psref  15370  mhmlin  15463  subm0cl  15471  eqger  15722  eqgcpbl  15726  gaorber  15817  orbstafun  15820  cayleyth  15911  pmtrrn2  15957  pmtrfinv  15958  dfod2  16056  sylow2blem1  16110  dprdf  16480  dprdff  16486  dprdfcl  16487  dprdffOLD  16492  dprdfclOLD  16493  dprdsplit  16537  dpjcntz  16541  ablfac1a  16560  ablfac1b  16561  rngsrg  16673  lmodvsdi  16951  lbssp  17140  2idlcpbl  17296  assarng  17372  mpff  17599  mpfaddcl  17600  mpfmulcl  17601  mpfind  17602  pf1rcl  17763  mpfpf1  17765  mdetunilem2  18399  mdetunilem5  18402  mdetunilem6  18403  pnfnei  18804  cnptop2  18827  lmcl  18881  lmcnp  18888  flimfil  19522  tlmlmod  19743  ustbasel  19761  ustincl  19762  ustinvel  19764  ustfilxp  19767  tusunif  19824  imasdsf1olem  19928  xmeter  19988  tmsds  20039  metustexhalfOLD  20118  metustexhalf  20119  nlmlmod  20239  qdensere  20329  blcvx  20355  tgqioo  20357  icccmplem2  20380  reconnlem1  20383  cnmpt2pc  20480  phtpcer  20547  phtpcco2  20551  pcohtpylem  20571  pcohtpy  20572  pcophtb  20581  om1addcl  20585  pi1blem  20591  pi1cpbl  20596  pi1grplem  20601  pi1inv  20604  pi1xfrf  20605  pi1xfr  20607  pi1xfrcnvlem  20608  pi1cof  20611  pi1coghm  20613  cphnlm  20671  cphsqrcl2  20685  tchcph  20732  lmcau  20803  bcthlem4  20818  minveclem4c  20892  minveclem2  20893  minveclem3b  20895  minveclem4  20899  minveclem6  20901  ivthicc  20922  ovolfsval  20934  ovollb2lem  20951  ovolshftlem1  20972  ovolscalem1  20976  ovolicc1  20979  ovolicc2lem2  20981  ovolicc2lem4  20983  ovolicc2lem5  20984  ovolicopnf  20987  ioombl1lem1  21019  ioombl1lem3  21021  ioombl1lem4  21022  uniioovol  21039  uniioombllem2a  21042  uniioombllem2  21043  uniioombllem3a  21044  uniioombllem3  21045  uniioombllem4  21046  uniioombllem6  21048  dyadmaxlem  21057  volivth  21067  vitalilem2  21069  vitalilem5  21072  i1frn  21135  itg2monolem1  21208  itgcnlem  21247  itgrevallem1  21252  itgreval  21254  itgle  21267  ibladd  21278  iblabslem  21285  itgspliticc  21294  itgsplitioo  21295  ditgcl  21313  ditgswap  21314  ditgsplitlem  21315  limcdif  21331  limcresi  21340  limccnp  21346  limccnp2  21347  limcco  21348  dvlip  21445  dvlip2  21447  dveq0  21452  dvgt0lem1  21454  dvivthlem1  21460  dvcnvrelem1  21469  dvcnvre  21471  dvfsumlem2  21479  ftc1lem1  21487  ftc1a  21489  ftc1lem4  21491  ftc2ditglem  21497  itgsubstlem  21500  ply1rem  21615  fta1glem1  21617  ig1pdvds  21628  plyrem  21751  facth  21752  fta1lem  21753  vieta1lem1  21756  vieta1lem2  21757  aaliou3lem3  21790  aaliou3lem4  21792  aaliou3lem7  21795  taylfvallem1  21802  tayl0  21807  taylply2  21813  radcnvle  21865  psercnlem2  21869  psercnlem1  21870  psercn  21871  pserdvlem1  21872  pserdvlem2  21873  abelth2  21887  coseq00topi  21944  coseq0negpitopi  21945  cosordlem  21967  tanord1  21973  efif1olem1  21978  loglesqr  22176  logreclem  22194  chordthmlem4  22210  quart1  22231  quartlem2  22233  quartlem3  22234  quartlem4  22235  quart  22236  acosbnd  22275  atancj  22285  atanlogsublem  22290  atantan  22298  atanbndlem  22300  dvatan  22310  atantayl  22312  rlimcnp2  22340  divsqrsumlem  22353  ftalem5  22394  ftalem7  22396  basellem4  22401  basellem5  22402  perfectlem2  22549  dchrinv  22580  chpdifbndlem1  22782  pntibndlem2  22820  pntlemc  22824  pntlema  22825  pntlemb  22826  pntlemg  22827  pntlemh  22828  pntlemq  22830  pntlemr  22831  pntlemj  22832  pntlemi  22833  pntlemf  22834  pntlemk  22835  pntlemo  22836  pntleme  22837  pntlem3  22838  pntleml  22840  abvcxp  22844  axtgpasch  22908  cgr3simp2  22953  colline  23032  wlkonwlk  23402  constr3pth  23514  eupaf1o  23559  grpoass  23658  vcsm  23895  nvf  24014  ssps  24096  minvecolem2  24244  minvecolem4c  24248  minvecolem4  24249  minvecolem5  24250  minvecolem6  24251  eigvec1  25334  eliccelico  26035  elicoelioo  26036  ogrpaddlt  26149  slmdvsdi  26199  slmdvs1  26204  cnre2csqlem  26309  lmxrge0  26351  rnlogbval  26428  nnlogbexp  26432  sigaclci  26544  difelsiga  26545  insiga  26549  measvnul  26589  sibfrn  26692  eulerpartlemt  26723  eulerpartlemmf  26727  tg5segofs  26966  subfacp1lem2a  27037  subfacp1lem3  27039  subfacp1lem4  27040  subfacp1lem5  27041  sconpht2  27096  sconpi1  27097  rescon  27104  cvmsss  27125  cvmsn0  27126  cvmlift2lem3  27163  cvmlift2lem7  27167  cvmliftphtlem  27175  cvmliftpht  27176  cvmlift3lem5  27181  cvmlift3lem6  27182  ghomgrplem  27277  ghomfo  27279  ghomgsg  27281  ibladdnc  28420  iblabsnclem  28426  ftc1cnnclem  28436  ftc1anc  28446  ftc2nc  28447  ivthALT  28501  heiborlem3  28683  iccbnd  28710  rngohom1  28745  idl0cl  28789  maxidlnr  28813  stoweidlem11  29777  stoweidlem31  29797  stoweidlem36  29802  stoweidlem38  29804  stoweidlem44  29810  stoweidlem62  29828  sigardiv  29868  sigarcol  29871  sharhght  29872  sigaradd  29873  cevathlem1  29874  cevathlem2  29875  cevath  29876  lelttrdi  30149  vfwlkniswwlkn  30311  Lemma2  30464  erclwwlknsym  30471  erclwwlkntr  30472  lshpne  32520  opococ  32733  opexmid  32745  hlclat  32896  lclkrslem2  35076