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  7311  erinxp  7445  resixp  7565  domssex  7739  cantnflem1a  8189  cantnflem1d  8192  cantnflem3  8195  cantnflem4  8196  fpwwe2lem7  9060  canthnumlem  9072  canthp1lem2  9077  wun0  9142  supmullem2  10578  supmul  10579  ixxdisj  11650  ixxun  11651  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  ubioo  11668  elicore  11687  iccgelb  11691  iccss2  11705  icodisj  11755  xov1plusxeqvd  11776  fldiv  12084  immul  13178  sqrtge0  13300  sqrtrege0  13407  icco1  13582  ruclem2  14262  ruclem3  14263  ruclem8  14267  ruclem12  14271  gcddvds  14451  crt  14686  phimullem  14687  eulerthlem1  14689  eulerthlem2  14690  prmreclem3  14816  sectcan  15602  sectco  15603  sectmon  15629  monsect  15630  funcixp  15714  funcsect  15719  invfuc  15821  coapm  15908  catciso  15944  posasymb  16140  ipodrsima  16353  pstr2  16393  psdmrn  16395  psref  16396  mhmlin  16531  subm0cl  16541  eqger  16809  eqgcpbl  16813  gaorber  16904  orbstafun  16907  cayleyth  16998  pmtrrn2  17043  pmtrfinv  17044  dfod2  17144  sylow2blem1  17198  dprdf  17564  dprdff  17571  dprdfcl  17572  dprdsplit  17607  dpjcntz  17611  ablfac1a  17628  ablfac1b  17629  lmodvsdi  18040  lbssp  18228  2idlcpbl  18384  assaring  18470  mpff  18682  mpfaddcl  18683  mpfmulcl  18684  mpfind  18685  pf1rcl  18863  mpfpf1  18865  mdetunilem2  19560  mdetunilem5  19563  mdetunilem6  19564  chfacfisfcpmat  19801  pnfnei  20158  cnptop2  20181  lmcl  20235  lmcnp  20242  flimfil  20906  tlmlmod  21125  ustbasel  21143  ustincl  21144  ustinvel  21146  ustfilxp  21149  tusunif  21206  imasdsf1olem  21310  xmeter  21370  tmsds  21421  metustexhalf  21493  nlmlmod  21603  qdensere  21692  blcvx  21718  tgqioo  21720  icccmplem2  21743  reconnlem1  21746  cnmpt2pc  21843  phtpcer  21910  phtpcco2  21914  pcohtpylem  21934  pcohtpy  21935  pcophtb  21944  om1addcl  21948  pi1blem  21954  pi1cpbl  21959  pi1grplem  21964  pi1inv  21967  pi1xfrf  21968  pi1xfr  21970  pi1xfrcnvlem  21971  pi1cof  21974  pi1coghm  21976  cphnlm  22034  cphsqrtcl2  22048  tchcph  22095  lmcau  22166  bcthlem4  22179  minveclem4c  22251  minveclem2  22252  minveclem3b  22254  minveclem4  22258  minveclem6  22260  ivthicc  22281  ovolfsval  22293  ovollb2lem  22310  ovolshftlem1  22331  ovolscalem1  22335  ovolicc1  22338  ovolicc2lem2  22340  ovolicc2lem4  22342  ovolicc2lem5  22343  ovolicopnf  22346  ioombl1lem1  22379  ioombl1lem3  22381  ioombl1lem4  22382  uniioovol  22404  uniioombllem2a  22407  uniioombllem2  22408  uniioombllem2OLD  22409  uniioombllem3a  22410  uniioombllem3  22411  uniioombllem4  22412  uniioombllem6  22414  dyadmaxlem  22423  volivth  22433  vitalilem2  22435  vitalilem5  22438  i1frn  22503  itg2monolem1  22576  itgcnlem  22615  itgrevallem1  22620  itgreval  22622  itgle  22635  ibladd  22646  iblabslem  22653  itgspliticc  22662  itgsplitioo  22663  ditgcl  22681  ditgswap  22682  ditgsplitlem  22683  limcdif  22699  limcresi  22708  limccnp  22714  limccnp2  22715  limcco  22716  dvlip  22813  dvlip2  22815  dveq0  22820  dvgt0lem1  22822  dvivthlem1  22828  dvcnvrelem1  22837  dvcnvre  22839  dvfsumlem2  22847  ftc1lem1  22855  ftc1a  22857  ftc1lem4  22859  ftc2ditglem  22865  itgsubstlem  22868  ply1rem  22980  fta1glem1  22982  ig1pdvds  22993  plyrem  23117  facth  23118  fta1lem  23119  vieta1lem1  23122  vieta1lem2  23123  aaliou3lem3  23156  aaliou3lem4  23158  aaliou3lem7  23161  taylfvallem1  23168  tayl0  23173  taylply2  23179  radcnvle  23231  psercnlem2  23235  psercnlem1  23236  psercn  23237  pserdvlem1  23238  pserdvlem2  23239  abelth2  23253  coseq00topi  23313  coseq0negpitopi  23314  cosordlem  23336  tanord1  23342  efif1olem1  23347  loglesqrt  23554  logreclem  23555  relogbval  23565  nnlogbexp  23574  chordthmlem4  23617  quart1  23638  quartlem2  23640  quartlem3  23641  quartlem4  23642  quart  23643  acosbnd  23682  atancj  23692  atanlogsublem  23697  atantan  23705  atanbndlem  23707  dvatan  23717  atantayl  23719  rlimcnp2  23748  divsqrtsumlem  23761  ftalem5  23857  ftalem7  23859  basellem4  23864  basellem5  23865  perfectlem2  24012  dchrinv  24043  chpdifbndlem1  24245  pntibndlem2  24283  pntlemc  24287  pntlema  24288  pntlemb  24289  pntlemg  24290  pntlemh  24291  pntlemq  24293  pntlemr  24294  pntlemj  24295  pntlemi  24296  pntlemf  24297  pntlemk  24298  pntlemo  24299  pntleme  24300  pntlem3  24301  pntleml  24303  abvcxp  24307  axtgpasch  24369  cgr3simp2  24419  legso  24495  hlne2  24502  hlln  24503  mirhl  24574  hlperpnel  24615  opphllem4  24640  inagswap  24724  wlkonwlk  25101  constr3pth  25224  vfwlkniswwlkn  25270  clwwlknscsh  25383  erclwwlknsym  25390  erclwwlkntr  25391  eupaf1o  25534  grpoass  25767  vcsm  26004  nvf  26123  ssps  26205  minvecolem2  26353  minvecolem4c  26357  minvecolem4  26358  minvecolem5  26359  minvecolem6  26360  eigvec1  27441  eliccelico  28186  elicoelioo  28187  slmdvsdi  28360  slmdvs1  28365  pmtrto1cl  28442  cnre2csqlem  28546  lmxrge0  28588  sigaclci  28784  difelsiga  28785  insiga  28789  ldsysgenld  28812  sigapildsyslem  28813  sigapildsys  28814  ldgenpisyslem1  28815  measvnul  28858  sibfrn  28989  eulerpartlemt  29021  eulerpartlemmf  29025  tg5segofs  29269  subfacp1lem2a  29682  subfacp1lem3  29684  subfacp1lem4  29685  subfacp1lem5  29686  sconpht2  29740  sconpi1  29741  rescon  29748  cvmsss  29769  cvmsn0  29770  cvmlift2lem3  29807  cvmlift2lem7  29811  cvmliftphtlem  29819  cvmliftpht  29820  cvmlift3lem5  29825  cvmlift3lem6  29826  msrf  29959  elmsta  29965  mclsax  29986  mthmpps  29999  mclspps  30001  ghomgrplem  30086  ghomfo  30088  ghomgsg  30090  ivthALT  30767  poimirlem17  31651  poimirlem20  31654  ibladdnc  31693  iblabsnclem  31699  ftc1cnnclem  31709  ftc1anc  31719  ftc2nc  31720  heiborlem3  31839  iccbnd  31866  rngohom1  31901  idl0cl  31945  maxidlnr  31969  lshpne  32247  opococ  32460  opexmid  32472  hlclat  32623  lclkrslem2  34805  cvgdvgrat  36289  iccshift  37194  iccsuble  37195  icoiccdif  37200  mullimc  37258  limccog  37262  mullimcf  37265  lptioo2  37273  limcmptdm  37277  limcicciooub  37279  icccncfext  37327  cncfioobdlem  37336  ditgeqiooicc  37396  itgsubsticc  37412  iblcncfioo  37414  itgiccshift  37416  itgperiod  37417  itgsbtaddcnst  37418  stoweidlem11  37430  stoweidlem31  37451  stoweidlem36  37456  stoweidlem38  37458  stoweidlem44  37464  stoweidlem62  37482  stoweidlem62OLD  37483  dirkercncflem1  37524  dirkercncflem4  37527  fourierdlem26  37554  fourierdlem32  37560  fourierdlem33  37561  fourierdlem37  37565  fourierdlem42  37570  fourierdlem54  37582  fourierdlem63  37591  fourierdlem64  37592  fourierdlem65  37593  fourierdlem69  37597  fourierdlem74  37602  fourierdlem75  37603  fourierdlem79  37607  fourierdlem81  37609  fourierdlem82  37610  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem93  37621  fourierdlem101  37629  fourierdlem111  37639  saldifcl  37717  sigardiv  37860  sigarcol  37863  sharhght  37864  sigaradd  37865  cevathlem1  37866  cevathlem2  37867  cevath  37868  perfectALTVlem2  38224  proththd  38294  lelttrdi  38386