Theorem simp2d 1074

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

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:  simp2bi  1077  f1dom3fv3dif  6525  f1dom3el3dif  6526  f1prex  6539  oeeui  7682  erinxp  7821  resixp  7943  domssex  8121  cantnflem1a  8582  cantnflem1d  8585  cantnflem3  8588  cantnflem4  8589  fpwwe2lem7  9458  canthnumlem  9470  canthp1lem2  9475  wun0  9540  lelttrdi  10199  supmullem2  10994  supmul  10995  ixxdisj  12190  ixxun  12191  ixxss1  12193  ixxss2  12194  ixxss12  12195  ixxub  12196  ixxlb  12197  ubioo  12207  elicore  12226  iccgelb  12230  iccss2  12244  icodisj  12297  xov1plusxeqvd  12318  fldiv  12659  immul  13876  sqrtge0  13998  sqrtrege0  14105  icco1  14271  ruclem2  14961  ruclem3  14962  ruclem8  14966  ruclem12  14970  gcddvds  15225  crth  15483  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  prmreclem3  15622  sectcan  16415  sectco  16416  sectmon  16442  monsect  16443  funcixp  16527  funcsect  16532  invfuc  16634  coapm  16721  catciso  16757  posasymb  16952  ipodrsima  17165  pstr2  17205  psdmrn  17207  psref  17208  mhmlin  17342  subm0cl  17352  eqger  17644  eqgcpbl  17648  gaorber  17741  orbstafun  17744  cayleyth  17835  pmtrrn2  17880  pmtrfinv  17881  dfod2  17981  sylow2blem1  18035  dprdf  18405  dprdff  18411  dprdfcl  18412  dprdsplit  18447  dpjcntz  18451  ablfac1a  18468  ablfac1b  18469  lmodvsdi  18886  lbssp  19079  2idlcpbl  19234  assaring  19320  mpff  19533  mpfaddcl  19534  mpfmulcl  19535  mpfind  19536  pf1rcl  19713  mpfpf1  19715  mdetunilem2  20419  mdetunilem5  20422  mdetunilem6  20423  chfacfisfcpmat  20660  pnfnei  21024  cnptop2  21047  lmcl  21101  lmcnp  21108  flimfil  21773  tlmlmod  21992  ustbasel  22010  ustincl  22011  ustinvel  22013  ustfilxp  22016  tusunif  22073  imasdsf1olem  22178  xmeter  22238  tmsds  22289  metustexhalf  22361  nlmlmod  22482  qdensere  22573  blcvx  22601  tgqioo  22603  icccmplem2  22626  reconnlem1  22629  cnmpt2pc  22727  phtpcer  22794  phtpcerOLD  22795  phtpcco2  22799  pcohtpylem  22819  pcohtpy  22820  pcophtb  22829  om1addcl  22833  pi1blem  22839  pi1cpbl  22844  pi1grplem  22849  pi1inv  22852  pi1xfrf  22853  pi1xfr  22855  pi1xfrcnvlem  22856  pi1cof  22859  pi1coghm  22861  cphnlm  22972  cphsqrtcl2  22986  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  ovolicc1  23284  ovolicc2lem2  23286  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicopnf  23292  ioombl1lem1  23326  ioombl1lem3  23328  ioombl1lem4  23329  uniioovol  23347  uniioombllem2a  23350  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  dyadmaxlem  23365  volivth  23375  vitalilem2  23378  vitalilem5  23381  i1frn  23444  itg2monolem1  23517  itgcnlem  23556  itgrevallem1  23561  itgreval  23563  itgle  23576  ibladd  23587  iblabslem  23594  itgspliticc  23603  itgsplitioo  23604  ditgcl  23622  ditgswap  23623  ditgsplitlem  23624  limcdif  23640  limcresi  23649  limccnp  23655  limccnp2  23656  limcco  23657  dvlip  23756  dvlip2  23758  dveq0  23763  dvgt0lem1  23765  dvivthlem1  23771  dvcnvrelem1  23780  dvcnvre  23782  dvfsumlem2  23790  ftc1lem1  23798  ftc1a  23800  ftc1lem4  23802  ftc2ditglem  23808  itgsubstlem  23811  ply1rem  23923  fta1glem1  23925  ig1pdvds  23936  plyrem  24060  facth  24061  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  aaliou3lem3  24099  aaliou3lem4  24101  aaliou3lem7  24104  taylfvallem1  24111  tayl0  24116  taylply2  24122  radcnvle  24174  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  abelth2  24196  coseq00topi  24254  coseq0negpitopi  24255  cosordlem  24277  tanord1  24283  efif1olem1  24288  loglesqrt  24499  logreclem  24500  relogbval  24510  nnlogbexp  24519  chordthmlem4  24562  quart1  24583  quartlem2  24585  quartlem3  24586  quartlem4  24587  quart  24588  acosbnd  24627  atancj  24637  atanlogsublem  24642  atantan  24650  atanbndlem  24652  dvatan  24662  atantayl  24664  rlimcnp2  24693  divsqrtsumlem  24706  ftalem5  24803  ftalem7  24805  basellem4  24810  basellem5  24811  perfectlem2  24955  dchrinv  24986  chpdifbndlem1  25242  pntibndlem2  25280  pntlemc  25284  pntlema  25285  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemi  25293  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntleme  25297  pntlem3  25298  pntleml  25300  abvcxp  25304  axtgpasch  25366  cgr3simp2  25416  legso  25494  hlne2  25501  hlln  25502  mirhl  25574  hlperpnel  25617  opphllem4  25642  inagswap  25730  subumgredg2  26177  upgrres1  26205  nb3grprlem1  26282  wlkp  26512  wspthsswwlkn  26814  2wlkdlem6  26827  clwwlknbp0  26884  clwwisshclwwsn  26929  erclwwlkseqlen  26933  erclwwlkssym  26935  erclwwlkstr  26936  extwwlkfablem1  27207  grpoass  27357  vcsm  27417  nvf  27515  ssps  27585  minvecolem2  27731  minvecolem4c  27735  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  eigvec1  28821  eliccelico  29539  elicoelioo  29540  slmdvsdi  29768  slmdvs1  29773  pmtrto1cl  29849  cnre2csqlem  29956  lmxrge0  29998  sigaclci  30195  difelsiga  30196  insiga  30200  ldsysgenld  30223  sigapildsyslem  30224  sigapildsys  30225  ldgenpisyslem1  30226  measvnul  30269  sibfrn  30399  eulerpartlemt  30433  eulerpartlemmf  30437  tg5segofs  30751  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem4  31165  subfacp1lem5  31166  sconnpht2  31220  sconnpi1  31221  resconn  31228  cvmsss  31249  cvmsn0  31250  cvmlift2lem3  31287  cvmlift2lem7  31291  cvmliftphtlem  31299  cvmliftpht  31300  cvmlift3lem5  31305  cvmlift3lem6  31306  msrf  31439  elmsta  31445  mclsax  31466  mthmpps  31479  mclspps  31481  scutun12  31917  slerec  31923  ivthALT  32330  poimirlem17  33426  poimirlem20  33429  ibladdnc  33467  iblabsnclem  33473  ftc1cnnclem  33483  ftc1anc  33493  ftc2nc  33494  heiborlem3  33612  iccbnd  33639  rngohom1  33767  idl0cl  33817  maxidlnr  33841  lshpne  34269  opococ  34482  opexmid  34494  hlclat  34645  lclkrslem2  36827  gneispacern2  38437  cvgdvgrat  38512  iccshift  39744  iccsuble  39745  icoiccdif  39750  mullimc  39848  limccog  39852  mullimcf  39855  lptioo2  39863  limcmptdm  39867  limcicciooub  39869  xlimmnfvlem1  40058  xlimpnfvlem1  40062  icccncfext  40100  cncfioobdlem  40109  ditgeqiooicc  40176  itgsubsticc  40192  iblcncfioo  40194  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem11  40228  stoweidlem31  40248  stoweidlem36  40253  stoweidlem38  40255  stoweidlem44  40261  stoweidlem62  40279  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem26  40350  fourierdlem32  40356  fourierdlem33  40357  fourierdlem37  40361  fourierdlem42  40366  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem69  40392  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem93  40416  fourierdlem101  40424  fourierdlem111  40434  saldifcl  40539  unisalgen2  40572  hoidmv1lelem3  40807  smff  40941  smfpimltxr  40956  sigardiv  41050  sigarcol  41053  sharhght  41054  sigaradd  41055  cevathlem1  41056  cevathlem2  41057  cevath  41058  proththd  41531  perfectALTVlem2  41631