Theorem simp3d 1143

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1137	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp3bi  1146  f1dom3fv3dif  7150  f1dom3el3dif  7151  oeeui  8442  resixp  8730  domssex2  8933  cantnflem1c  9454  cantnflem1  9456  cantnflem3  9458  cantnflem4  9459  fpwwe2lem6  10401  canthnumlem  10413  canthp1lem2  10418  wununi  10471  wunpw  10472  wunpr  10474  lelttrdi  11146  ixxdisj  13103  ixxun  13104  ixxss1  13106  ixxss2  13107  ixxss12  13108  ixxub  13109  ixxlb  13110  lbioo  13119  elicore  13140  iccsupr  13183  icodisj  13217  xov1plusxeqvd  13239  intfracq  13588  fldiv  13589  seqf1olem2  13772  cjmul  14862  icco1  15258  sumtp  15470  rpnnen2lem10  15941  ruclem2  15950  ruclem3  15951  ruclem9  15956  ruclem12  15959  dvdslegcd  16220  crth  16488  eulerthlem1  16491  eulerthlem2  16492  pcpremul  16553  prmreclem2  16627  prmreclem3  16628  4sqlem13  16667  sectcan  17476  sectco  17477  sectmon  17503  monsect  17504  funcid  17594  funcco  17595  funcsect  17596  invfuc  17701  fuciso  17702  coapm  17795  catciso  17835  postr  18047  ipodrsima  18268  psref2  18297  psasym  18303  mhm0  18447  submcl  18460  submmnd  18461  eqger  18815  eqgcpbl  18819  gaorber  18923  orbsta  18928  cayleyth  19032  pmtrrn2  19077  pmtrfinv  19078  pmtrfmvdn0  19079  dfod2  19180  sylow2blem1  19234  sylow2blem3  19236  dprdcntz  19620  dprddisj  19621  dprdffsupp  19626  dpjdisj  19665  ablfac1a  19681  ablfac1b  19682  lmodvsdir  20156  lmhmlin  20306  lbsind  20351  2idlcpbl  20514  assasca  21078  mpfind  21326  mdetunilem2  21771  mdetunilem5  21774  mdetunilem6  21775  mnfnei  22381  cnprcl  22405  lmcvg  22422  lmff  22461  lmcls  22462  lmcnp  22464  fbasssin  22996  flimfil  23129  tgpconncomp  23273  tlmtrg  23350  ustssel  23366  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ustfilxp  23373  tustopn  23432  tususp  23433  imasdsf1olem  23535  xmeter  23595  xmetresbl  23599  tmstopn  23650  metustexhalf  23721  nlmnrg  23852  qdensere  23942  blcvx  23970  tgqioo  23972  icccmplem1  23994  icccmplem2  23995  reconnlem1  23998  cnmpopc  24100  iccpnfcnv  24116  phtpcer  24167  phtpcco2  24171  pcohtpy  24192  pcorev2  24200  pcophtb  24201  om1addcl  24205  pi1blem  24211  pi1cpbl  24216  pi1grplem  24221  pi1inv  24224  pi1xfrf  24225  pi1xfr  24227  pi1xfrcnvlem  24228  pi1cof  24231  pi1coghm  24233  cphreccllem  24351  cphsca  24352  cphsubrg  24353  cphsqrtcl2  24359  phclm  24405  tcphcph  24410  lmmcvg  24434  cmetcaulem  24461  lmcau  24486  bcthlem3  24499  bcthlem4  24500  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  ivthicc  24631  ovollb2lem  24661  ovolshftlem1  24682  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem2  24691  ovolicc2lem3  24692  ovolicc2lem4  24693  ovolicc2lem5  24694  ioombl1lem1  24731  dyadmaxlem  24770  volivth  24780  vitalilem2  24782  vitalilem4  24784  i1fima2  24852  itg2monolem1  24924  itgcnlem  24963  itgrevallem1  24968  itgreval  24970  itgle  24983  ibladd  24994  iblabslem  25001  itgspliticc  25010  itgsplitioo  25011  ditgcl  25031  ditgswap  25032  ditgsplitlem  25033  limcdif  25049  limcresi  25058  limcres  25059  limccnp  25064  limccnp2  25065  limcun  25068  dvlip  25166  dvlip2  25168  dveq0  25173  dvgt0lem1  25175  dvivthlem1  25181  dvcnvrelem1  25190  dvcnvre  25192  dvfsumlem2  25200  ftc1lem1  25208  ftc1lem2  25209  ftc1a  25210  ftc1lem4  25212  ftc2  25217  ftc2ditglem  25218  itgsubstlem  25221  ply1rem  25337  fta1glem2  25340  ig1pdvds  25350  plyrem  25474  fta1lem  25476  vieta1lem2  25480  aaliou3lem3  25513  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  abelth2  25610  coseq00topi  25668  coseq0negpitopi  25669  cosordlem  25695  tanord1  25702  efif1olem1  25707  dvloglem  25812  efopnlem1  25820  logreclem  25921  relogbval  25931  nnlogbexp  25940  logbrec  25941  chordthmlem4  25994  quart1  26015  quartlem2  26017  quartlem3  26018  quart  26020  acosbnd  26059  atancj  26069  atanlogsublem  26074  atantan  26082  atanbndlem  26084  atans2  26090  dvatan  26094  atantayl  26096  divsqrtsumlem  26138  ftalem5  26235  basellem5  26243  ppisval  26262  chtleppi  26367  chpchtsum  26376  chpub  26377  mersenne  26384  perfectlem2  26387  dchrinv  26418  rplogsumlem2  26642  chpdifbndlem1  26710  pntibndlem2  26748  pntlema  26753  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemr  26759  pntlemj  26760  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntlemp  26767  pntleml  26768  abvcxp  26772  ostth2lem2  26791  axtgcont1  26838  cgr3simp3  26892  legso  26969  hlln  26977  hltr  26980  btwnhl  26984  mirhl  27049  mirbtwnhl  27050  opphllem4  27120  opphl  27124  hlpasch  27126  cgracgr  27188  cgraswap  27190  cgrahl  27197  cgracol  27198  inagswap  27211  inagne3  27214  dfcgrg2  27233  umgrnloopv  27485  umgredgne  27524  usgrnloopvALT  27577  frusgrnn0  27947  cusgrm1rusgr  27958  upgrclwlkcompim  28158  2wlkdlem6  28305  2wlkond  28311  2trlond  28313  numclwwlk2lem1  28749  numclwlk2lem2f1o  28752  tncp  28849  grpolidinv  28872  nvs  29034  nvz  29040  nvtri  29041  sspn  29107  minvecolem2  29246  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  adj1  30304  eliccelico  31107  elicoelioo  31108  prmdvdsbc  31139  pmtrto1cl  31375  cyc3evpm  31426  slmdvsdir  31478  slmd0vs  31486  nsgqusf1olem3  31609  prmidl  31624  prmidlc  31633  qsidomlem2  31638  mxidlmax  31646  locfinreflem  31799  cnre2csqlem  31869  sigaclci  32109  unelsiga  32111  insiga  32114  unelldsys  32135  ldsysgenld  32137  sigapildsys  32139  ldgenpisyslem1  32140  measvun  32186  cntmeas  32203  sibfima  32314  signstfveq0  32565  tg5segofs  32662  bnj1018g  32952  bnj1018  32953  pfxwlk  33094  revwlk  33095  spthcycl  33100  acycgrcycl  33118  subfacp1lem3  33153  subfacp1lem4  33154  subfacp1lem5  33155  sconnpht2  33209  sconnpi1  33210  txsconn  33212  resconn  33217  cvmcn  33233  cvmsuni  33240  cvmsdisj  33241  cvmshmeo  33242  cvmlift2lem8  33281  cvmlift2lem13  33286  cvmliftphtlem  33288  cvmliftpht  33289  cvmlift3lem6  33295  msrf  33513  elmsta  33519  mthmpps  33553  mclsppslem  33554  scutun12  34013  slerec  34022  cofcut2  34100  cofcutr  34101  cofcutrtime  34102  ivthALT  34533  relowlssretop  35543  ibladdnc  35843  iblabsnclem  35849  ftc2nc  35868  dvasin  35870  isbndx  35949  isbnd3  35951  prdsbnd  35960  heiborlem3  35980  iccbnd  36007  rngohomadd  36136  rngohommul  36137  idladdcl  36186  idllmulcl  36187  idlrmulcl  36188  maxidlmax  36210  pridlc  36238  eqvreltr  36727  lshpnelb  37005  lshpcmp  37009  oplecon3  37220  opnoncon  37229  hlcvl  37380  dochshpncl  39405  lclkrslem1  39558  lclkrslem2  39559  fzne2d  39996  sticksstones3  40111  metakunt8  40139  metakunt20  40151  metakunt21  40152  metakunt22  40153  metakunt24  40155  metakunt25  40156  evlsval3  40279  flt4lem5f  40501  flt4lem7  40503  nna4b4nsq  40504  acongrep  40809  ntrneinex  41694  neicvgmex  41734  gneispace0nelrn  41757  cvgdvgrat  41938  binomcxplemdvbinom  41978  eliocre  43054  iccshift  43063  iccsuble  43064  icoiccdif  43069  mullimc  43164  limccog  43168  limciccioolb  43169  mullimcf  43171  limcperiod  43176  lptioo2  43179  lptioo1  43180  neglimc  43195  addlimc  43196  0ellimcdiv  43197  reclimc  43201  xlimmnfvlem1  43380  xlimpnfvlem1  43384  icccncfext  43435  cncfioobdlem  43444  ditgeqiooicc  43508  iblspltprt  43521  iblcncfioo  43526  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem11  43559  stoweidlem31  43579  stoweidlem36  43584  stoweidlem38  43586  stoweidlem62  43610  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem26  43681  fourierdlem32  43687  fourierdlem33  43688  fourierdlem37  43692  fourierdlem42  43697  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem74  43728  fourierdlem75  43729  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem93  43747  fourierdlem101  43755  fourierdlem107  43761  fourierdlem109  43763  fourierdlem111  43765  salunicl  43864  saluncl  43865  hoidmv1lelem1  44136  hoidmv1lelem3  44138  hoidmvlelem1  44140  ovolval3  44192  iinhoiicclem  44218  smfpreimalt  44276  smfpreimaltf  44281  smfpreimale  44299  issmfgt  44301  smfpreimagt  44307  smfpreimage  44327  sigardiv  44388  sigarcol  44391  sharhght  44392  sigaradd  44393  cevathlem1  44394  cevathlem2  44395  cevath  44396  proththd  45077  perfectALTVlem2  45185