Theorem simp3d 1075

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
simp3d	|- ( ph -> th )

Proof of Theorem simp3d

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

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:  simp3bi  1078  f1dom3fv3dif  6525  f1dom3el3dif  6526  oeeui  7682  erinxp  7821  resixp  7943  domssex2  8120  cantnflem1c  8584  cantnflem1  8586  cantnflem3  8588  cantnflem4  8589  fpwwe2lem7  9458  canthnumlem  9470  canthp1lem2  9475  wununi  9528  wunpw  9529  wunpr  9531  lelttrdi  10199  ixxdisj  12190  ixxun  12191  ixxss1  12193  ixxss2  12194  ixxss12  12195  ixxub  12196  ixxlb  12197  lbioo  12206  elicore  12226  iccsupr  12266  icodisj  12297  xov1plusxeqvd  12318  intfracq  12658  fldiv  12659  seqf1olem2  12841  cjmul  13882  icco1  14271  sumtp  14478  rpnnen2lem10  14952  ruclem2  14961  ruclem3  14962  ruclem9  14967  ruclem12  14970  dvdslegcd  15226  crth  15483  eulerthlem1  15486  eulerthlem2  15487  pcpremul  15548  prmreclem2  15621  prmreclem3  15622  4sqlem13  15661  sectcan  16415  sectco  16416  sectmon  16442  monsect  16443  funcid  16530  funcco  16531  funcsect  16532  invfuc  16634  fuciso  16635  coapm  16721  catciso  16757  postr  16953  ipodrsima  17165  psref2  17204  psasym  17210  mhm0  17343  submcl  17353  submmnd  17354  eqger  17644  eqgcpbl  17648  gaorber  17741  orbsta  17746  cayleyth  17835  pmtrrn2  17880  pmtrfinv  17881  pmtrfmvdn0  17882  dfod2  17981  sylow2blem1  18035  sylow2blem3  18037  dprdcntz  18407  dprddisj  18408  dprdffsupp  18413  dpjdisj  18452  ablfac1a  18468  ablfac1b  18469  lmodvsdir  18887  lmhmlin  19035  lbsind  19080  2idlcpbl  19234  assasca  19321  mpfind  19536  mpt2frlmd  20116  mdetunilem2  20419  mdetunilem5  20422  mdetunilem6  20423  mnfnei  21025  cnprcl  21049  lmcvg  21066  lmff  21105  lmcls  21106  lmcnp  21108  fbasssin  21640  flimfil  21773  tgpconncomp  21916  tlmtrg  21993  ustssel  22009  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ustfilxp  22016  tustopn  22075  tususp  22076  imasdsf1olem  22178  xmeter  22238  xmetresbl  22242  tmstopn  22290  metustexhalf  22361  nlmnrg  22483  qdensere  22573  blcvx  22601  tgqioo  22603  icccmplem1  22625  icccmplem2  22626  reconnlem1  22629  cnmpt2pc  22727  iccpnfcnv  22743  phtpcer  22794  phtpcerOLD  22795  phtpcco2  22799  pcohtpy  22820  pcorev2  22828  pcophtb  22829  om1addcl  22833  pi1blem  22839  pi1cpbl  22844  pi1grplem  22849  pi1inv  22852  pi1xfrf  22853  pi1xfr  22855  pi1xfrcnvlem  22856  pi1cof  22859  pi1coghm  22861  cphreccllem  22978  cphsca  22979  cphsubrg  22980  cphsqrtcl2  22986  tchclm  23031  tchcph  23036  lmmcvg  23059  cmetcaulem  23086  lmcau  23111  bcthlem3  23123  bcthlem4  23124  minveclem4c  23196  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  ivthicc  23227  ovollb2lem  23256  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  ioombl1lem1  23326  dyadmaxlem  23365  volivth  23375  vitalilem2  23378  vitalilem4  23380  i1fima2  23446  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  limcres  23650  limccnp  23655  limccnp2  23656  limcun  23659  dvlip  23756  dvlip2  23758  dveq0  23763  dvgt0lem1  23765  dvivthlem1  23771  dvcnvrelem1  23780  dvcnvre  23782  dvfsumlem2  23790  ftc1lem1  23798  ftc1lem2  23799  ftc1a  23800  ftc1lem4  23802  ftc2  23807  ftc2ditglem  23808  itgsubstlem  23811  ply1rem  23923  fta1glem2  23926  ig1pdvds  23936  plyrem  24060  fta1lem  24062  vieta1lem2  24066  aaliou3lem3  24099  pserulm  24176  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  abelth2  24196  coseq00topi  24254  coseq0negpitopi  24255  cosordlem  24277  tanord1  24283  efif1olem1  24288  dvloglem  24394  efopnlem1  24402  logreclem  24500  relogbval  24510  nnlogbexp  24519  logbrec  24520  chordthmlem4  24562  quart1  24583  quartlem2  24585  quartlem3  24586  quart  24588  acosbnd  24627  atancj  24637  atanlogsublem  24642  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  divsqrtsumlem  24706  ftalem5  24803  basellem5  24811  ppisval  24830  chtleppi  24935  chpchtsum  24944  chpub  24945  mersenne  24952  perfectlem2  24955  dchrinv  24986  rplogsumlem2  25174  chpdifbndlem1  25242  pntibndlem2  25280  pntlema  25285  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlemp  25299  pntleml  25300  abvcxp  25304  ostth2lem2  25323  axtgcont1  25367  cgr3simp3  25417  legso  25494  hlln  25502  hltr  25505  btwnhl  25509  mirhl  25574  mirbtwnhl  25575  opphllem4  25642  opphl  25646  hlpasch  25648  cgracgr  25710  cgraswap  25712  cgrahl  25718  cgracol  25719  inagswap  25730  umgrnloopv  26001  umgredgne  26040  usgrnloopvALT  26093  frusgrnn0  26467  cusgrm1rusgr  26478  upgrclwlkcompim  26677  2wlkdlem6  26827  2wlkond  26833  2trlond  26835  numclwwlk2lem1  27235  tncp  27330  grpolidinv  27355  nvs  27518  nvz  27524  nvtri  27525  sspn  27591  minvecolem2  27731  minvecolem4c  27735  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  adj1  28792  eliccelico  29539  elicoelioo  29540  slmdvsdir  29769  slmd0vs  29777  pmtrto1cl  29849  locfinreflem  29907  cnre2csqlem  29956  sigaclci  30195  unelsiga  30197  insiga  30200  unelldsys  30221  ldsysgenld  30223  sigapildsys  30225  ldgenpisyslem1  30226  measvun  30272  cntmeas  30289  sibfima  30400  signstfveq0  30654  tg5segofs  30751  bnj1018  31032  subfacp1lem3  31164  subfacp1lem4  31165  subfacp1lem5  31166  sconnpht2  31220  sconnpi1  31221  txsconn  31223  resconn  31228  cvmcn  31244  cvmsuni  31251  cvmsdisj  31252  cvmshmeo  31253  cvmlift2lem8  31292  cvmlift2lem13  31297  cvmliftphtlem  31299  cvmliftpht  31300  cvmlift3lem6  31306  msrf  31439  elmsta  31445  mthmpps  31479  mclsppslem  31480  scutun12  31917  slerec  31923  ivthALT  32330  relowlssretop  33211  ibladdnc  33467  iblabsnclem  33473  ftc2nc  33494  dvasin  33496  isbndx  33581  isbnd3  33583  prdsbnd  33592  heiborlem3  33612  iccbnd  33639  rngohomadd  33768  rngohommul  33769  idladdcl  33818  idllmulcl  33819  idlrmulcl  33820  maxidlmax  33842  pridlc  33870  lshpnelb  34271  lshpcmp  34275  oplecon3  34486  opnoncon  34495  hlcvl  34646  dochshpncl  36673  lclkrslem1  36826  lclkrslem2  36827  acongrep  37547  ntrneinex  38375  neicvgmex  38415  gneispace0nelrn  38438  cvgdvgrat  38512  binomcxplemdvbinom  38552  eliocre  39734  iccshift  39744  iccsuble  39745  icoiccdif  39750  mullimc  39848  limccog  39852  limciccioolb  39853  mullimcf  39855  limcperiod  39860  lptioo2  39863  lptioo1  39864  neglimc  39879  addlimc  39880  0ellimcdiv  39881  reclimc  39885  xlimmnfvlem1  40058  xlimpnfvlem1  40062  icccncfext  40100  cncfioobdlem  40109  ditgeqiooicc  40176  iblspltprt  40189  iblcncfioo  40194  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem11  40228  stoweidlem31  40248  stoweidlem36  40253  stoweidlem38  40255  stoweidlem62  40279  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem26  40350  fourierdlem32  40356  fourierdlem33  40357  fourierdlem37  40361  fourierdlem42  40366  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem93  40416  fourierdlem101  40424  fourierdlem107  40430  fourierdlem109  40432  fourierdlem111  40434  salunicl  40536  saluncl  40537  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmvlelem1  40809  ovolval3  40861  iinhoiicclem  40887  smfpreimalt  40940  smfpreimaltf  40945  smfpreimale  40963  issmfgt  40965  smfpreimagt  40970  smfpreimage  40990  sigardiv  41050  sigarcol  41053  sharhght  41054  sigaradd  41055  cevathlem1  41056  cevathlem2  41057  cevath  41058  proththd  41531  perfectALTVlem2  41631