Theorem simp2d 994

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

Syntax hints:   -> wi 4   /\ w3a 958

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 960

This theorem is referenced by:  simp2bi  997  f1dom3fv3dif  5967  f1dom3el3dif  5968  oeeui  7029  erinxp  7162  resixp  7286  domssex  7460  cantnflem1a  7881  cantnflem1d  7884  cantnflem3  7887  cantnflem4  7888  cantnflem1aOLD  7904  cantnflem1dOLD  7907  cantnflem3OLD  7909  cantnflem4OLD  7910  fpwwe2lem7  8790  canthnumlem  8802  canthp1lem2  8807  wun0  8872  supmullem2  10284  supmul  10285  ixxdisj  11302  ixxun  11303  ixxss1  11305  ixxss2  11306  ixxss12  11307  ixxub  11308  ixxlb  11309  ubioo  11319  iccgelb  11339  iccss2  11353  icodisj  11396  xov1plusxeqvd  11417  fldiv  11682  immul  12608  sqrge0  12730  sqrrege0  12836  icco1  13001  ruclem2  13496  ruclem3  13497  ruclem8  13501  ruclem12  13505  gcddvds  13681  crt  13835  phimullem  13836  eulerthlem1  13838  eulerthlem2  13839  prmreclem3  13961  sectcan  14676  sectco  14677  sectmon  14698  monsect  14699  funcixp  14759  funcsect  14764  invfuc  14866  coapm  14921  catciso  14957  posasymb  15104  ipodrsima  15317  pstr2  15357  psdmrn  15359  psref  15360  mhmlin  15453  subm0cl  15461  eqger  15710  eqgcpbl  15714  gaorber  15805  orbstafun  15808  cayleyth  15899  pmtrrn2  15945  pmtrfinv  15946  dfod2  16044  sylow2blem1  16098  dprdf  16463  dprdff  16469  dprdfcl  16470  dprdffOLD  16475  dprdfclOLD  16476  dprdsplit  16520  dpjcntz  16524  ablfac1a  16543  ablfac1b  16544  lmodvsdi  16894  lbssp  17081  2idlcpbl  17237  assarng  17313  mdetunilem2  18260  mdetunilem5  18263  mdetunilem6  18264  pnfnei  18665  cnptop2  18688  lmcl  18742  lmcnp  18749  flimfil  19383  tlmlmod  19604  ustbasel  19622  ustincl  19623  ustinvel  19625  ustfilxp  19628  tusunif  19685  imasdsf1olem  19789  xmeter  19849  tmsds  19900  metustexhalfOLD  19979  metustexhalf  19980  nlmlmod  20100  qdensere  20190  blcvx  20216  tgqioo  20218  icccmplem2  20241  reconnlem1  20244  cnmpt2pc  20341  phtpcer  20408  phtpcco2  20412  pcohtpylem  20432  pcohtpy  20433  pcophtb  20442  om1addcl  20446  pi1blem  20452  pi1cpbl  20457  pi1grplem  20462  pi1inv  20465  pi1xfrf  20466  pi1xfr  20468  pi1xfrcnvlem  20469  pi1cof  20472  pi1coghm  20474  cphnlm  20532  cphsqrcl2  20546  tchcph  20593  lmcau  20664  bcthlem4  20679  minveclem4c  20753  minveclem2  20754  minveclem3b  20756  minveclem4  20760  minveclem6  20762  ivthicc  20783  ovolfsval  20795  ovollb2lem  20812  ovolshftlem1  20833  ovolscalem1  20837  ovolicc1  20840  ovolicc2lem2  20842  ovolicc2lem4  20844  ovolicc2lem5  20845  ovolicopnf  20848  ioombl1lem1  20880  ioombl1lem3  20882  ioombl1lem4  20883  uniioovol  20900  uniioombllem2a  20903  uniioombllem2  20904  uniioombllem3a  20905  uniioombllem3  20906  uniioombllem4  20907  uniioombllem6  20909  dyadmaxlem  20918  volivth  20928  vitalilem2  20930  vitalilem5  20933  i1frn  20996  itg2monolem1  21069  itgcnlem  21108  itgrevallem1  21113  itgreval  21115  itgle  21128  ibladd  21139  iblabslem  21146  itgspliticc  21155  itgsplitioo  21156  ditgcl  21174  ditgswap  21175  ditgsplitlem  21176  limcdif  21192  limcresi  21201  limccnp  21207  limccnp2  21208  limcco  21209  dvlip  21306  dvlip2  21308  dveq0  21313  dvgt0lem1  21315  dvivthlem1  21321  dvcnvrelem1  21330  dvcnvre  21332  dvfsumlem2  21340  ftc1lem1  21348  ftc1a  21350  ftc1lem4  21352  ftc2ditglem  21358  itgsubstlem  21361  mpff  21392  mpfaddcl  21393  mpfmulcl  21394  mpfind  21395  pf1rcl  21399  mpfpf1  21401  ply1rem  21519  fta1glem1  21521  ig1pdvds  21532  plyrem  21655  facth  21656  fta1lem  21657  vieta1lem1  21660  vieta1lem2  21661  aaliou3lem3  21694  aaliou3lem4  21696  aaliou3lem7  21699  taylfvallem1  21706  tayl0  21711  taylply2  21717  radcnvle  21769  psercnlem2  21773  psercnlem1  21774  psercn  21775  pserdvlem1  21776  pserdvlem2  21777  abelth2  21791  coseq00topi  21848  coseq0negpitopi  21849  cosordlem  21871  tanord1  21877  efif1olem1  21882  loglesqr  22080  logreclem  22098  chordthmlem4  22114  quart1  22135  quartlem2  22137  quartlem3  22138  quartlem4  22139  quart  22140  acosbnd  22179  atancj  22189  atanlogsublem  22194  atantan  22202  atanbndlem  22204  dvatan  22214  atantayl  22216  rlimcnp2  22244  divsqrsumlem  22257  ftalem5  22298  ftalem7  22300  basellem4  22305  basellem5  22306  perfectlem2  22453  dchrinv  22484  chpdifbndlem1  22686  pntibndlem2  22724  pntlemc  22728  pntlema  22729  pntlemb  22730  pntlemg  22731  pntlemh  22732  pntlemq  22734  pntlemr  22735  pntlemj  22736  pntlemi  22737  pntlemf  22738  pntlemk  22739  pntlemo  22740  pntleme  22741  pntlem3  22742  pntleml  22744  abvcxp  22748  axtgpasch  22812  cgr3simp2  22853  colline  22917  wlkonwlk  23256  constr3pth  23368  eupaf1o  23413  grpoass  23512  vcsm  23749  nvf  23868  ssps  23950  minvecolem2  24098  minvecolem4c  24102  minvecolem4  24103  minvecolem5  24104  minvecolem6  24105  eigvec1  25188  eliccelico  25889  elicoelioo  25890  ogrpaddlt  26004  rngsrg  26042  slmdvsdi  26079  slmdvs1  26084  cnre2csqlem  26193  lmxrge0  26235  rnlogbval  26312  nnlogbexp  26316  sigaclci  26428  difelsiga  26429  insiga  26433  measvnul  26473  sibfrn  26570  eulerpartlemt  26601  eulerpartlemmf  26605  tg5segofs  26844  subfacp1lem2a  26915  subfacp1lem3  26917  subfacp1lem4  26918  subfacp1lem5  26919  sconpht2  26974  sconpi1  26975  rescon  26982  cvmsss  27003  cvmsn0  27004  cvmlift2lem3  27041  cvmlift2lem7  27045  cvmliftphtlem  27053  cvmliftpht  27054  cvmlift3lem5  27059  cvmlift3lem6  27060  ghomgrplem  27154  ghomfo  27156  ghomgsg  27158  ibladdnc  28290  iblabsnclem  28296  ftc1cnnclem  28306  ftc1anc  28316  ftc2nc  28317  ivthALT  28371  heiborlem3  28553  iccbnd  28580  rngohom1  28615  idl0cl  28659  maxidlnr  28683  stoweidlem11  29649  stoweidlem31  29669  stoweidlem36  29674  stoweidlem38  29676  stoweidlem44  29682  stoweidlem62  29700  sigardiv  29740  sigarcol  29743  sharhght  29744  sigaradd  29745  cevathlem1  29746  cevathlem2  29747  cevath  29748  lelttrdi  30021  vfwlkniswwlkn  30183  Lemma2  30336  erclwwlknsym  30343  erclwwlkntr  30344  lshpne  32197  opococ  32410  opexmid  32422  hlclat  32573  lclkrslem2  34753