Theorem simp1d 1073

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
simp1d	|- ( ph -> ps )

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp1 1061	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
3	1, 2	syl 17	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simp1bi  1076  f1dom3fv3dif  6525  f1dom3el3dif  6526  f1prex  6539  oeeui  7682  oeeu  7683  erinxp  7821  domssex2  8120  domssex  8121  cantnflem1a  8582  cantnflem1b  8583  cantnflem1c  8584  cantnflem1d  8585  cantnflem1  8586  cantnflem3  8588  cantnflem4  8589  fpwwe2lem7  9458  canthnumlem  9470  canthp1lem2  9475  wuntr  9527  lelttrdi  10199  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  ixxdisj  12190  ixxun  12191  ixxss1  12193  ixxss2  12194  ixxss12  12195  ixxub  12196  ixxlb  12197  iccss2  12244  iocssre  12253  icossre  12254  iccssre  12255  icodisj  12297  iccf1o  12316  xov1plusxeqvd  12318  fzen  12358  intfracq  12658  fldiv  12659  remul  13869  sqrlem6  13988  resqrtth  13996  sqrtth  14104  ruclem6  14964  ruclem9  14967  ruclem12  14970  gcdn0cl  15224  crth  15483  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  pcpremul  15548  prmreclem3  15622  sectcan  16415  sectco  16416  sectmon  16442  monsect  16443  funcf1  16526  funcsect  16532  invfuc  16634  coapm  16721  catciso  16757  psrel  17203  pstr  17211  mhmf  17340  submss  17350  eqger  17644  eqgcpbl  17648  gaorber  17741  orbstafun  17744  cayleyth  17835  dprdgrp  18404  dprdff  18411  ablfac1a  18468  ablfac1b  18469  lmodvscl  18880  lbsss  19077  2idlcpbl  19234  assalmod  19319  mpfind  19536  mdetunilem2  20419  mdetunilem5  20422  mdetunilem6  20423  chfacfisfcpmat  20660  cnptop1  21046  lmfpm  21099  lmff  21105  lmcnp  21108  flimtop  21769  tlmtmd  21990  ustssxp  22008  ustdiag  22012  ustfilxp  22016  ustbas2  22029  tusbas  22072  imasdsf1olem  22178  xmeter  22238  tmsbas  22288  metustexhalf  22361  nlmngp  22481  qdensere  22573  blcvx  22601  tgqioo  22603  icccmplem2  22626  reconnlem1  22629  cnmpt2pc  22727  icoopnst  22738  iocopnst  22739  iccpnfcnv  22743  phtpcer  22794  phtpcerOLD  22795  phtpcco2  22799  pcohtpylem  22819  pcohtpy  22820  pcopt  22822  pcopt2  22823  pcorevlem  22826  pcorev2  22828  pcophtb  22829  om1addcl  22833  pi1cpbl  22844  pi1grplem  22849  pi1inv  22852  pi1xfrf  22853  pi1xfr  22855  pi1xfrcnvlem  22856  pi1xfrcnv  22857  pi1cof  22859  pi1coghm  22861  cphphl  22971  cphreccllem  22978  cphsqrtcl2  22986  tchclm  23031  tchcph  23036  lmcau  23111  bcthlem4  23124  minveclem4c  23196  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  ivthicc  23227  ovolfsval  23239  ovollb2lem  23256  ovolshftlem1  23277  ovolscalem1  23281  ovolicc2lem2  23286  ovolicc2lem5  23289  ovolicopnf  23292  ioombl1lem1  23326  ioombl1lem3  23328  ioombl1lem4  23329  uniioovol  23347  uniioombllem2a  23350  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  i1ff  23443  itg2monolem1  23517  itgreval  23563  ibladd  23587  iblabslem  23594  itgspliticc  23603  itgsplitioo  23604  ditgcl  23622  ditgswap  23623  ditgsplitlem  23624  ditgsplit  23625  limcresi  23649  dvlip2  23758  dveq0  23763  dvcnvre  23782  dvfsumlem2  23790  ftc1a  23800  ply1rem  23923  facth1  23924  fta1glem1  23925  fta1glem2  23926  ig1pcl  23935  ig1pdvds  23936  plyrem  24060  facth  24061  vieta1lem1  24065  vieta1lem2  24066  aaliou3lem3  24099  aaliou3lem7  24104  pserulm  24176  psercnlem2  24178  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  abelth2  24196  coseq00topi  24254  coseq0negpitopi  24255  cosordlem  24277  efif1olem1  24288  dvloglem  24394  loglesqrt  24499  relogbval  24510  nnlogbexp  24519  logbrec  24520  quart1  24583  quartlem2  24585  quartlem3  24586  quartlem4  24587  quart  24588  asinsinlem  24618  atanlogsublem  24642  atans2  24658  dvatan  24662  rlimcnp2  24693  divsqrtsumlem  24706  ftalem5  24803  ftalem7  24805  basellem4  24810  basellem5  24811  perfectlem2  24955  dchrinv  24986  chpdifbndlem1  25242  pntibndlem2  25280  pntlema  25285  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemn  25289  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlemp  25299  pntleml  25300  abvcxp  25304  axtgbtwnid  25365  cgr3simp1  25415  hlne1  25500  hltr  25505  btwnhl  25509  mirhl  25574  opphllem4  25642  hlpasch  25648  inagswap  25730  wlkf  26510  wlk1ewlk  26536  2wlkdlem6  26827  2wlkond  26833  2trlond  26835  grpofo  27353  vcablo  27424  nvvc  27470  sspba  27582  sspg  27583  minvecolem2  27731  minvecolem4c  27735  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  eleigveccl  28818  xrofsup  29533  eliccelico  29539  elicoelioo  29540  slmdvscl  29767  slmdvsass  29770  baselsiga  30178  insiga  30200  ldsysgenld  30223  sigapildsys  30225  ldgenpisyslem1  30226  measfrge0  30266  sibfmbl  30397  eulerpartlemt  30433  eulerpartlemmf  30437  probfinmeasbOLD  30490  tg5segofs  30751  subfacp1lem2a  31162  subfacp1lem2b  31163  subfacp1lem3  31164  subfacp1lem4  31165  subfacp1lem5  31166  sconnpht2  31220  sconnpi1  31221  cvxsconn  31225  cvmlift2lem3  31287  cvmlift2lem5  31289  cvmlift2lem6  31290  cvmlift2lem7  31291  cvmlift2lem12  31296  cvmliftphtlem  31299  cvmliftpht  31300  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3lem5  31305  cvmlift3lem6  31306  msrf  31439  elmsta  31445  mthmpps  31479  mclsppslem  31480  mclspps  31481  scutun12  31917  scutf  31919  slerec  31923  sltrec  31924  madeval2  31936  iblabsnclem  33473  dvasin  33496  isbnd3  33583  heiborlem3  33612  iccbnd  33639  rngohomf  33765  idlss  33815  lshplss  34268  opoccl  34481  opococ  34482  oplecon3  34486  hloml  34644  lclkrslem1  36826  lclkrslem2  36827  eliccre  39728  eliocre  39734  icoiccdif  39750  limccog  39852  lptioo1  39864  cncfiooicclem1  40106  ditgeqiooicc  40176  stoweidlem30  40247  stoweidlem31  40248  stoweidlem38  40255  stoweidlem44  40261  fourierdlem26  40350  fourierdlem32  40356  fourierdlem33  40357  fourierdlem37  40361  fourierdlem42  40366  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem69  40392  fourierdlem79  40402  fourierdlem82  40405  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem111  40434  0sal  40540  hoidmv1lelem3  40807  smfdmss  40942  smfpimltxr  40956  sigardiv  41050  sigarcol  41053  sharhght  41054  sigaradd  41055  cevathlem1  41056  cevathlem2  41057  cevath  41058  proththd  41531  perfectALTVlem2  41631