Theorem simp2d 1018

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

Syntax hints:   -> wi 4   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  simp2bi  1021  f1dom3fv3dif  6183  f1dom3el3dif  6184  f1prex  6197  oeeui  7314  erinxp  7448  resixp  7568  domssex  7742  cantnflem1a  8198  cantnflem1d  8201  cantnflem3  8204  cantnflem4  8205  fpwwe2lem7  9068  canthnumlem  9080  canthp1lem2  9085  wun0  9150  supmullem2  10585  supmul  10586  ixxdisj  11657  ixxun  11658  ixxss1  11660  ixxss2  11661  ixxss12  11662  ixxub  11663  ixxlb  11664  ixxlbOLD  11665  ubioo  11675  elicore  11694  iccgelb  11698  iccss2  11712  icodisj  11764  xov1plusxeqvd  11785  fldiv  12093  immul  13199  sqrtge0  13321  sqrtrege0  13428  icco1  13603  ruclem2  14283  ruclem3  14284  ruclem8  14288  ruclem12  14292  gcddvds  14476  crt  14725  phimullem  14726  eulerthlem1  14728  eulerthlem2  14729  prmreclem3  14861  sectcan  15659  sectco  15660  sectmon  15686  monsect  15687  funcixp  15771  funcsect  15776  invfuc  15878  coapm  15965  catciso  16001  posasymb  16197  ipodrsima  16410  pstr2  16450  psdmrn  16452  psref  16453  mhmlin  16588  subm0cl  16598  eqger  16866  eqgcpbl  16870  gaorber  16961  orbstafun  16964  cayleyth  17055  pmtrrn2  17100  pmtrfinv  17101  dfod2  17214  sylow2blem1  17271  dprdf  17637  dprdff  17644  dprdfcl  17645  dprdsplit  17680  dpjcntz  17684  ablfac1a  17701  ablfac1b  17702  lmodvsdi  18113  lbssp  18301  2idlcpbl  18457  assaring  18543  mpff  18755  mpfaddcl  18756  mpfmulcl  18757  mpfind  18758  pf1rcl  18936  mpfpf1  18938  mdetunilem2  19636  mdetunilem5  19639  mdetunilem6  19640  chfacfisfcpmat  19877  pnfnei  20234  cnptop2  20257  lmcl  20311  lmcnp  20318  flimfil  20982  tlmlmod  21201  ustbasel  21219  ustincl  21220  ustinvel  21222  ustfilxp  21225  tusunif  21282  imasdsf1olem  21386  xmeter  21446  tmsds  21497  metustexhalf  21569  nlmlmod  21679  qdensere  21788  blcvx  21814  tgqioo  21816  icccmplem2  21839  reconnlem1  21842  cnmpt2pc  21954  phtpcer  22024  phtpcco2  22028  pcohtpylem  22048  pcohtpy  22049  pcophtb  22058  om1addcl  22062  pi1blem  22068  pi1cpbl  22073  pi1grplem  22078  pi1inv  22081  pi1xfrf  22082  pi1xfr  22084  pi1xfrcnvlem  22085  pi1cof  22088  pi1coghm  22090  cphnlm  22148  cphsqrtcl2  22162  tchcph  22209  lmcau  22280  bcthlem4  22293  minveclem4c  22365  minveclem2  22366  minveclem3b  22368  minveclem4  22372  minveclem6  22374  minveclem4cOLD  22377  minveclem2OLD  22378  minveclem3bOLD  22380  minveclem4OLD  22384  minveclem6OLD  22386  ivthicc  22407  ovolfsval  22421  ovollb2lem  22439  ovolshftlem1  22460  ovolscalem1  22464  ovolicc1  22467  ovolicc2lem2  22469  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  ovolicopnf  22476  ioombl1lem1  22509  ioombl1lem3  22511  ioombl1lem4  22512  uniioovol  22534  uniioombllem2a  22537  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem3a  22540  uniioombllem3  22541  uniioombllem4  22542  uniioombllem6  22544  dyadmaxlem  22553  volivth  22563  vitalilem2  22565  vitalilem5  22568  i1frn  22633  itg2monolem1  22706  itgcnlem  22745  itgrevallem1  22750  itgreval  22752  itgle  22765  ibladd  22776  iblabslem  22783  itgspliticc  22792  itgsplitioo  22793  ditgcl  22811  ditgswap  22812  ditgsplitlem  22813  limcdif  22829  limcresi  22838  limccnp  22844  limccnp2  22845  limcco  22846  dvlip  22943  dvlip2  22945  dveq0  22950  dvgt0lem1  22952  dvivthlem1  22958  dvcnvrelem1  22967  dvcnvre  22969  dvfsumlem2  22977  ftc1lem1  22985  ftc1a  22987  ftc1lem4  22989  ftc2ditglem  22995  itgsubstlem  22998  ply1rem  23112  fta1glem1  23114  ig1pdvds  23126  ig1pdvdsOLD  23132  plyrem  23256  facth  23257  fta1lem  23258  vieta1lem1  23261  vieta1lem2  23262  aaliou3lem3  23298  aaliou3lem4  23300  aaliou3lem7  23303  taylfvallem1  23310  tayl0  23315  taylply2  23321  radcnvle  23373  psercnlem2  23377  psercnlem1  23378  psercn  23379  pserdvlem1  23380  pserdvlem2  23381  abelth2  23395  coseq00topi  23455  coseq0negpitopi  23456  cosordlem  23478  tanord1  23484  efif1olem1  23489  loglesqrt  23696  logreclem  23697  relogbval  23707  nnlogbexp  23716  chordthmlem4  23759  quart1  23780  quartlem2  23782  quartlem3  23783  quartlem4  23784  quart  23785  acosbnd  23824  atancj  23834  atanlogsublem  23839  atantan  23847  atanbndlem  23849  dvatan  23859  atantayl  23861  rlimcnp2  23890  divsqrtsumlem  23903  ftalem5  23999  ftalem5OLD  24001  ftalem7  24003  basellem4  24008  basellem5  24009  perfectlem2  24156  dchrinv  24187  chpdifbndlem1  24389  pntibndlem2  24427  pntlemc  24431  pntlema  24432  pntlemb  24433  pntlemg  24434  pntlemh  24435  pntlemq  24437  pntlemr  24438  pntlemj  24439  pntlemi  24440  pntlemf  24441  pntlemk  24442  pntlemo  24443  pntleme  24444  pntlem3  24445  pntleml  24447  abvcxp  24451  axtgpasch  24513  cgr3simp2  24564  legso  24642  hlne2  24649  hlln  24650  mirhl  24722  hlperpnel  24765  opphllem4  24790  inagswap  24878  wlkonwlk  25263  constr3pth  25386  vfwlkniswwlkn  25432  clwwlknscsh  25545  erclwwlknsym  25552  erclwwlkntr  25553  eupaf1o  25696  grpoass  25929  vcsm  26166  nvf  26285  ssps  26367  minvecolem2  26515  minvecolem4c  26519  minvecolem4  26520  minvecolem5  26521  minvecolem6  26522  minvecolem2OLD  26525  minvecolem4cOLD  26529  minvecolem4OLD  26530  minvecolem5OLD  26531  minvecolem6OLD  26532  eigvec1  27613  eliccelico  28365  elicoelioo  28366  slmdvsdi  28538  slmdvs1  28543  pmtrto1cl  28620  cnre2csqlem  28724  lmxrge0  28766  sigaclci  28962  difelsiga  28963  insiga  28967  ldsysgenld  28990  sigapildsyslem  28991  sigapildsys  28992  ldgenpisyslem1  28993  measvnul  29036  sibfrn  29178  eulerpartlemt  29212  eulerpartlemmf  29216  tg5segofs  29498  subfacp1lem2a  29911  subfacp1lem3  29913  subfacp1lem4  29914  subfacp1lem5  29915  sconpht2  29969  sconpi1  29970  rescon  29977  cvmsss  29998  cvmsn0  29999  cvmlift2lem3  30036  cvmlift2lem7  30040  cvmliftphtlem  30048  cvmliftpht  30049  cvmlift3lem5  30054  cvmlift3lem6  30055  msrf  30188  elmsta  30194  mclsax  30215  mthmpps  30228  mclspps  30230  ghomgrplem  30315  ghomfo  30317  ghomgsg  30319  ivthALT  30996  poimirlem17  31921  poimirlem20  31924  ibladdnc  31963  iblabsnclem  31969  ftc1cnnclem  31979  ftc1anc  31989  ftc2nc  31990  heiborlem3  32109  iccbnd  32136  rngohom1  32171  idl0cl  32215  maxidlnr  32239  lshpne  32517  opococ  32730  opexmid  32742  hlclat  32893  lclkrslem2  35075  cvgdvgrat  36632  iccshift  37568  iccsuble  37569  icoiccdif  37574  mullimc  37636  limccog  37640  mullimcf  37643  lptioo2  37651  limcmptdm  37655  limcicciooub  37657  icccncfext  37705  cncfioobdlem  37714  ditgeqiooicc  37777  itgsubsticc  37793  iblcncfioo  37795  itgiccshift  37797  itgperiod  37798  itgsbtaddcnst  37799  stoweidlem11  37811  stoweidlem31  37832  stoweidlem36  37837  stoweidlem38  37839  stoweidlem44  37845  stoweidlem62  37863  stoweidlem62OLD  37864  dirkercncflem1  37905  dirkercncflem4  37908  fourierdlem26  37935  fourierdlem32  37942  fourierdlem33  37943  fourierdlem37  37947  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem54  37964  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem69  37979  fourierdlem74  37984  fourierdlem75  37985  fourierdlem79  37989  fourierdlem81  37991  fourierdlem82  37992  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem93  38003  fourierdlem101  38011  fourierdlem111  38021  saldifcl  38101  hoidmv1lelem3  38319  sigardiv  38341  sigarcol  38344  sharhght  38345  sigaradd  38346  cevathlem1  38347  cevathlem2  38348  cevath  38349  perfectALTVlem2  38714  proththd  38784  lelttrdi  38901  umgrres1  39149  nb3grprlem1  39214