Theorem simp3d 1144

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 1138	. 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7211  f1dom3el3dif  7212  oeeui  8526  resixp  8866  domssex2  9060  cantnflem1c  9587  cantnflem1  9589  cantnflem3  9591  cantnflem4  9592  fpwwe2lem6  10537  canthnumlem  10549  canthp1lem2  10554  wununi  10607  wunpw  10608  wunpr  10610  lelttrdi  11285  ixxdisj  13270  ixxun  13271  ixxss1  13273  ixxss2  13274  ixxss12  13275  ixxub  13276  ixxlb  13277  lbioo  13286  elicore  13308  iccsupr  13352  icodisj  13386  xov1plusxeqvd  13408  intfracq  13773  fldiv  13774  seqf1olem2  13959  cjmul  15059  icco1  15457  sumtp  15666  rpnnen2lem10  16142  ruclem2  16151  ruclem3  16152  ruclem9  16157  ruclem12  16160  dvdslegcd  16425  prmdvdsbc  16647  crth  16699  eulerthlem1  16702  eulerthlem2  16703  pcpremul  16765  prmreclem2  16839  prmreclem3  16840  4sqlem13  16879  sectcan  17672  sectco  17673  sectmon  17699  monsect  17700  funcid  17787  funcco  17788  funcsect  17789  invfuc  17894  fuciso  17895  coapm  17988  catciso  18028  postr  18236  ipodrsima  18457  psref2  18486  psasym  18492  mhm0  18712  submcl  18730  submmnd  18731  eqger  19100  eqgcpbl  19104  ghmqusnsglem1  19202  ghmquskerlem1  19205  gaorber  19230  orbsta  19235  cayleyth  19337  pmtrrn2  19382  pmtrfinv  19383  pmtrfmvdn0  19384  dfod2  19486  sylow2blem1  19542  sylow2blem3  19544  dprdcntz  19932  dprddisj  19933  dprdffsupp  19938  dpjdisj  19977  ablfac1a  19993  ablfac1b  19994  lmodvsdir  20829  lmhmlin  20979  lbsind  21024  2idlcpblrng  21218  mpfind  22052  mdetunilem2  22538  mdetunilem5  22541  mdetunilem6  22542  mnfnei  23146  cnprcl  23170  lmcvg  23187  lmff  23226  lmcls  23227  lmcnp  23229  fbasssin  23761  flimfil  23894  tgpconncomp  24038  tlmtrg  24115  ustssel  24131  ustincl  24133  ustdiag  24134  ustinvel  24135  ustexhalf  24136  ustfilxp  24138  tustopn  24195  tususp  24196  imasdsf1olem  24298  xmeter  24358  xmetresbl  24362  tmstopn  24410  metustexhalf  24481  nlmnrg  24604  qdensere  24694  blcvx  24723  tgqioo  24725  icccmplem1  24748  icccmplem2  24749  reconnlem1  24752  cnmpopc  24859  iccpnfcnv  24879  phtpcer  24931  phtpcco2  24936  pcohtpy  24957  pcorev2  24965  pcophtb  24966  om1addcl  24970  pi1blem  24976  pi1cpbl  24981  pi1grplem  24986  pi1inv  24989  pi1xfrf  24990  pi1xfr  24992  pi1xfrcnvlem  24993  pi1cof  24996  pi1coghm  24998  cphreccllem  25115  cphsca  25116  cphsubrg  25117  cphsqrtcl2  25123  phclm  25169  tcphcph  25174  lmmcvg  25198  cmetcaulem  25225  lmcau  25250  bcthlem3  25263  bcthlem4  25264  minveclem4c  25362  minveclem2  25363  minveclem3b  25365  minveclem4  25369  minveclem6  25371  ivthicc  25396  ovollb2lem  25426  ovolshftlem1  25447  ovolscalem1  25451  ovolicc1  25454  ovolicc2lem2  25456  ovolicc2lem3  25457  ovolicc2lem4  25458  ovolicc2lem5  25459  ioombl1lem1  25496  dyadmaxlem  25535  volivth  25545  vitalilem2  25547  vitalilem4  25549  i1fima2  25617  itg2monolem1  25688  itgcnlem  25728  itgrevallem1  25733  itgreval  25735  itgle  25748  ibladd  25759  iblabslem  25766  itgspliticc  25775  itgsplitioo  25776  ditgcl  25796  ditgswap  25797  ditgsplitlem  25798  limcdif  25814  limcresi  25823  limcres  25824  limccnp  25829  limccnp2  25830  limcun  25833  dvlip  25935  dvlip2  25937  dveq0  25942  dvgt0lem1  25944  dvivthlem1  25950  dvcnvrelem1  25959  dvcnvre  25961  dvfsumlem2  25970  dvfsumlem2OLD  25971  ftc1lem1  25979  ftc1lem2  25980  ftc1a  25981  ftc1lem4  25983  ftc2  25988  ftc2ditglem  25989  itgsubstlem  25992  ply1rem  26108  fta1glem2  26111  ig1pdvds  26122  plyrem  26250  fta1lem  26252  vieta1lem2  26256  aaliou3lem3  26289  pserulm  26368  psercnlem2  26371  psercnlem1  26372  psercn  26373  pserdvlem1  26374  pserdvlem2  26375  abelth2  26389  coseq00topi  26448  coseq0negpitopi  26449  cosordlem  26476  tanord1  26483  efif1olem1  26488  dvloglem  26594  efopnlem1  26602  logreclem  26709  relogbval  26719  nnlogbexp  26728  logbrec  26729  chordthmlem4  26782  quart1  26803  quartlem2  26805  quartlem3  26806  quart  26808  acosbnd  26847  atancj  26857  atanlogsublem  26862  atantan  26870  atanbndlem  26872  atans2  26878  dvatan  26882  atantayl  26884  divsqrtsumlem  26927  ftalem5  27024  basellem5  27032  ppisval  27051  chtleppi  27158  chpchtsum  27167  chpub  27168  mersenne  27175  perfectlem2  27178  dchrinv  27209  rplogsumlem2  27433  chpdifbndlem1  27501  pntibndlem2  27539  pntlema  27544  pntlemb  27545  pntlemg  27546  pntlemh  27547  pntlemr  27550  pntlemj  27551  pntlemf  27553  pntlemk  27554  pntlemo  27555  pntlemp  27558  pntleml  27559  abvcxp  27563  ostth2lem2  27582  scutun12  27761  slerec  27770  eqscut3  27775  cofcut2  27876  cofcutr  27878  cofcutrtime  27881  cutmax  27888  cutmin  27889  addsproplem5  27926  addsproplem6  27927  sleadd1  27942  addsuniflem  27954  addsasslem1  27956  addsasslem2  27957  negsproplem4  27983  negsproplem6  27985  negscut2  27992  negsunif  28007  mulsproplem12  28076  ssltmul1  28096  ssltmul2  28097  mulsuniflem  28098  precsexlem11  28165  twocut  28356  pw2cut2  28392  axtgcont1  28456  cgr3simp3  28510  legso  28587  hlln  28595  hltr  28598  btwnhl  28602  mirhl  28667  mirbtwnhl  28668  opphllem4  28738  opphl  28742  hlpasch  28744  cgracgr  28806  cgraswap  28808  cgrahl  28815  cgracol  28816  inagswap  28829  inagne3  28832  dfcgrg2  28851  umgrnloopv  29095  umgredgne  29134  usgrnloopvALT  29190  frusgrnn0  29561  cusgrm1rusgr  29572  upgrclwlkcompim  29770  2wlkdlem6  29920  2wlkond  29926  2trlond  29928  numclwwlk2lem1  30367  numclwlk2lem2f1o  30370  tncp  30469  grpolidinv  30492  nvs  30654  nvz  30660  nvtri  30661  sspn  30727  minvecolem2  30866  minvecolem4c  30870  minvecolem4  30871  minvecolem5  30872  minvecolem6  30873  adj1  31924  eliccelico  32771  elicoelioo  32772  pmtrto1cl  33079  cyc3evpm  33130  slmdvsdir  33196  slmd0vs  33204  sdrgdvcl  33276  sdrginvcl  33277  nsgqusf1olem3  33391  prmidl  33416  prmidlc  33424  qsidomlem2  33429  qsnzr  33431  mxidlmax  33441  qsdrnglem2  33472  0ringmon1p  33531  ig1pmindeg  33573  ply1degltdimlem  33646  irngss  33711  ply1annig1p  33728  minplycl  33730  algextdeglem3  33743  algextdeglem4  33744  constrsqrtcl  33803  locfinreflem  33864  cnre2csqlem  33934  sigaclci  34156  unelsiga  34158  insiga  34161  unelldsys  34182  ldsysgenld  34184  sigapildsys  34186  ldgenpisyslem1  34187  measvun  34233  cntmeas  34250  sibfima  34362  signstfveq0  34601  tg5segofs  34697  bnj1018g  34986  bnj1018  34987  pfxwlk  35179  revwlk  35180  spthcycl  35184  acycgrcycl  35202  subfacp1lem3  35237  subfacp1lem4  35238  subfacp1lem5  35239  sconnpht2  35293  sconnpi1  35294  txsconn  35296  resconn  35301  cvmcn  35317  cvmsuni  35324  cvmsdisj  35325  cvmshmeo  35326  cvmlift2lem8  35365  cvmlift2lem13  35370  cvmliftphtlem  35372  cvmliftpht  35373  cvmlift3lem6  35379  msrf  35597  elmsta  35603  mthmpps  35637  mclsppslem  35638  ivthALT  36390  weiunfrlem  36519  weiunfr  36522  relowlssretop  37418  ibladdnc  37727  iblabsnclem  37733  ftc2nc  37752  dvasin  37754  isbndx  37832  isbnd3  37834  prdsbnd  37843  heiborlem3  37863  iccbnd  37890  rngohomadd  38019  rngohommul  38020  idladdcl  38069  idllmulcl  38070  idlrmulcl  38071  maxidlmax  38093  pridlc  38121  eqvreltr  38713  lshpnelb  39093  lshpcmp  39097  oplecon3  39308  opnoncon  39317  hlcvl  39468  dochshpncl  41493  lclkrslem1  41646  lclkrslem2  41647  fzne2d  42083  primrootsunit1  42200  primrootscoprmpow  42202  primrootlekpowne0  42208  aks6d1c1p1  42210  aks6d1c2  42233  sticksstones3  42251  aks5lem1  42289  aks5lem2  42290  aks5lem3a  42292  evlsval3  42667  flt4lem5f  42765  flt4lem7  42767  nna4b4nsq  42768  acongrep  43087  ntrneinex  44184  neicvgmex  44224  gneispace0nelrn  44247  cvgdvgrat  44420  binomcxplemdvbinom  44460  eliocre  45623  iccshift  45632  iccsuble  45633  icoiccdif  45638  mullimc  45730  limccog  45734  limciccioolb  45735  mullimcf  45737  limcperiod  45742  lptioo2  45745  lptioo1  45746  neglimc  45759  addlimc  45760  0ellimcdiv  45761  reclimc  45765  xlimmnfvlem1  45944  xlimpnfvlem1  45948  icccncfext  45999  cncfioobdlem  46008  ditgeqiooicc  46072  iblspltprt  46085  iblcncfioo  46090  itgiccshift  46092  itgperiod  46093  itgsbtaddcnst  46094  stoweidlem11  46123  stoweidlem31  46143  stoweidlem36  46148  stoweidlem38  46150  stoweidlem62  46174  dirkercncflem1  46215  dirkercncflem4  46218  fourierdlem26  46245  fourierdlem32  46251  fourierdlem33  46252  fourierdlem37  46256  fourierdlem42  46261  fourierdlem54  46272  fourierdlem63  46281  fourierdlem64  46282  fourierdlem65  46283  fourierdlem74  46292  fourierdlem75  46293  fourierdlem79  46297  fourierdlem81  46299  fourierdlem82  46300  fourierdlem89  46307  fourierdlem90  46308  fourierdlem91  46309  fourierdlem93  46311  fourierdlem101  46319  fourierdlem107  46325  fourierdlem109  46327  fourierdlem111  46329  salunicl  46428  saluncl  46429  hoidmv1lelem1  46703  hoidmv1lelem3  46705  hoidmvlelem1  46707  ovolval3  46759  iinhoiicclem  46785  smfpreimalt  46843  smfpreimaltf  46848  smfpreimale  46866  issmfgt  46868  smfpreimagt  46874  smfpreimage  46894  sigardiv  46973  sigarcol  46976  sharhght  46977  sigaradd  46978  cevathlem1  46979  cevathlem2  46980  cevath  46981  proththd  47728  perfectALTVlem2  47836  gpgnbgrvtx0  48188  gpgnbgrvtx1  48189  imasubc2  49267  imaf1co  49270  idfullsubc  49276  fucofulem1  49425