Theorem simp3d 1162

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 1156	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp3bi  1165  f1dom3fv3dif  7264  f1dom3el3dif  7265  oeeui  8595  resixp  8945  domssex2  9140  cantnflem1c  9672  cantnflem1  9674  cantnflem3  9676  cantnflem4  9677  fpwwe2lem6  10699  canthnumlem  10711  canthp1lem2  10716  wununi  10769  wunpw  10770  wunpr  10772  lelttrdi  11450  ixxdisj  13469  ixxun  13470  ixxss1  13472  ixxss2  13473  ixxss12  13474  ixxub  13475  ixxlb  13476  lbioo  13485  elicore  13507  iccsupr  13551  icodisj  13585  xov1plusxeqvd  13607  intfracq  13976  fldiv  13977  seqf1olem2  14162  cjmul  15286  icco1  15684  sumtp  15892  rpnnen2lem10  16368  ruclem2  16377  ruclem3  16378  ruclem9  16383  ruclem12  16386  dvdslegcd  16651  prmdvdsbc  16879  crth  16932  eulerthlem1  16935  eulerthlem2  16936  pcpremul  16998  prmreclem2  17072  prmreclem3  17073  4sqlem13  17112  sectcan  17907  sectco  17908  sectmon  17934  monsect  17935  funcid  18022  funcco  18023  funcsect  18024  invfuc  18129  fuciso  18130  coapm  18223  catciso  18263  postr  18471  ipodrsima  18692  psref2  18721  psasym  18727  mhm0  18966  submcl  18984  submmnd  18986  eqger  19367  eqgcpbl  19371  ghmqusnsglem1  19471  ghmquskerlem1  19474  gaorber  19499  orbsta  19504  cayleyth  19606  pmtrrn2  19651  pmtrfinv  19652  pmtrfmvdn0  19653  dfod2  19755  sylow2blem1  19811  sylow2blem3  19813  dprdcntz  20201  dprddisj  20202  dprdffsupp  20207  dpjdisj  20246  ablfac1a  20262  ablfac1b  20263  lmodvsdir  21138  lmhmlin  21287  lbsind  21332  2idlcpblrng  21542  prmidl  21598  prmidlc  21606  prmidlprop  21609  qsidomlem2  21614  qsnzr  21616  evlsval3  22375  mpfind  22401  mdetunilem2  22905  mdetunilem5  22908  mdetunilem6  22909  mnfnei  23516  cnprcl  23540  lmcvg  23557  lmff  23596  lmcls  23597  lmcnp  23599  fbasssin  24132  flimfil  24265  tgpconncomp  24409  tlmtrg  24486  ustssel  24502  ustincl  24504  ustdiag  24505  ustinvel  24506  ustexhalf  24507  ustfilxp  24509  tustopn  24566  tususp  24567  imasdsf1olem  24669  xmeter  24729  xmetresbl  24733  tmstopn  24781  metustexhalf  24852  nlmnrg  24975  qdensere  25065  blcvx  25094  tgqioo  25096  icccmplem1  25119  icccmplem2  25120  reconnlem1  25123  cnmpopc  25226  iccpnfcnv  25242  phtpcer  25293  phtpcco2  25297  pcohtpy  25318  pcorev2  25326  pcophtb  25327  om1addcl  25331  pi1blem  25337  pi1cpbl  25342  pi1grplem  25347  pi1inv  25350  pi1xfrf  25351  pi1xfr  25353  pi1xfrcnvlem  25354  pi1cof  25357  pi1coghm  25359  cphreccllem  25476  cphsca  25477  cphsubrg  25478  cphsqrtcl2  25484  phclm  25530  tcphcph  25535  lmmcvg  25559  cmetcaulem  25586  lmcau  25611  bcthlem3  25624  bcthlem4  25625  minveclem4c  25723  minveclem2  25724  minveclem3b  25726  minveclem4  25730  minveclem6  25732  ivthicc  25756  ovollb2lem  25786  ovolshftlem1  25807  ovolscalem1  25811  ovolicc1  25814  ovolicc2lem2  25816  ovolicc2lem3  25817  ovolicc2lem4  25818  ovolicc2lem5  25819  ioombl1lem1  25856  dyadmaxlem  25895  volivth  25905  vitalilem2  25907  vitalilem4  25909  i1fima2  25977  itg2monolem1  26048  itgcnlem  26087  itgrevallem1  26092  itgreval  26094  itgle  26107  ibladd  26118  iblabslem  26125  itgspliticc  26134  itgsplitioo  26135  ditgcl  26155  ditgswap  26156  ditgsplitlem  26157  limcdif  26173  limcresi  26182  limcres  26183  limccnp  26188  limccnp2  26189  limcun  26192  dvlip  26290  dvlip2  26292  dveq0  26297  dvgt0lem1  26299  dvivthlem1  26305  dvcnvrelem1  26314  dvcnvre  26316  dvfsumlem2  26324  ftc1lem1  26332  ftc1lem2  26333  ftc1a  26334  ftc1lem4  26336  ftc2  26341  ftc2ditglem  26342  itgsubstlem  26345  ply1rem  26461  fta1glem2  26464  ig1pdvds  26475  plyrem  26605  fta1lem  26607  vieta1lem2  26613  aaliou3lem3  26650  pserulm  26728  psercnlem2  26730  psercnlem1  26731  psercn  26732  pserdvlem1  26733  pserdvlem2  26734  abelth2  26748  coseq00topi  26810  coseq0negpitopi  26811  cosordlem  26837  tanord1  26844  efif1olem1  26849  dvloglem  26955  efopnlem1  26963  logreclem  27069  relogbval  27079  nnlogbexp  27088  logbrec  27089  chordthmlem4  27142  quart1  27163  quartlem2  27165  quartlem3  27166  quart  27168  acosbnd  27207  atancj  27217  atanlogsublem  27222  atantan  27230  atanbndlem  27232  atans2  27238  dvatan  27242  atantayl  27244  divsqrtsumlem  27286  ftalem5  27383  basellem5  27391  ppisval  27410  chtleppi  27516  chpchtsum  27525  chpub  27526  mersenne  27533  perfectlem2  27536  dchrinv  27567  rplogsumlem2  27791  chpdifbndlem1  27859  pntibndlem2  27897  pntlema  27902  pntlemb  27903  pntlemg  27904  pntlemh  27905  pntlemr  27908  pntlemj  27909  pntlemf  27911  pntlemk  27912  pntlemo  27913  pntlemp  27916  pntleml  27917  abvcxp  27921  ostth2lem2  27940  flt4lem5f  27966  flt4lem7  27968  nna4b4nsq  27969  cutsun12  28155  lesrec  28164  eqcuts3  28169  cofcut2  28287  cofcutr  28289  cofcutrtime  28292  cutmax  28299  cutmin  28300  addsproplem5  28338  addsproplem6  28339  leadds1  28354  addsuniflem  28366  addsasslem1  28368  addsasslem2  28369  negsproplem4  28396  negsproplem6  28398  negcut2  28405  negsunif  28420  mulsproplem12  28492  sltmuls1  28512  sltmuls2  28513  mulsuniflem  28514  precsexlem11  28582  twocut  28788  pw2cut2  28827  axtgcont1  28909  cgr3simp3  28964  legso  29041  hlln  29052  hltr  29055  btwnhl  29059  tghlsub  29065  mirhl  29130  mirbtwnhl  29131  opphllem4  29205  opphl  29209  hlpasch  29213  cgracgr  29304  cgraswap  29306  cgrahl  29314  cgracol  29315  inagswap  29339  inagne3  29342  dfcgrg2  29387  umgrnloopv  29663  umgredgne  29702  usgrnloopvALT  29761  frusgrnn0  30131  cusgrm1rusgr  30142  pfxwlk  30245  revwlk  30246  upgrclwlkcompim  30347  spthcycl  30371  2wlkdlem6  30499  2wlkond  30505  2trlond  30507  acycgrcycl  30732  numclwwlk2lem1  30956  numclwlk2lem2f1o  30959  tncp  31059  grpolidinv  31082  nvs  31244  nvz  31250  nvtri  31251  sspn  31317  minvecolem2  31456  minvecolem4c  31460  minvecolem4  31461  minvecolem5  31462  minvecolem6  31463  adj1  32514  eliccelico  33348  elicoelioo  33349  pmtrto1cl  33639  cyc3evpm  33690  slmdvsdir  33756  slmd0vs  33764  sdrgdvcl  33840  sdrginvcl  33841  nsgqusf1olem3  33945  mxidlmax  33969  qsdrnglem2  33999  0ringmon1p  34068  ig1pmindeg  34113  ply1degltdimlem  34233  irngss  34298  ply1annig1p  34315  minplycl  34317  algextdeglem3  34330  algextdeglem4  34331  constrsqrtcl  34390  locfinreflem  34451  cnre2csqlem  34521  sigaclci  34743  unelsiga  34745  insiga  34749  unelldsys  34770  ldsysgenld  34772  sigapildsys  34774  ldgenpisyslem1  34775  measvun  34821  cntmeas  34838  sibfima  34950  signstfveq0  35186  cgranbtwn  35278  tg5segofs  35285  bnj1018g  35573  bnj1018  35574  subfacp1lem3  35913  subfacp1lem4  35914  subfacp1lem5  35915  sconnpht2  35969  sconnpi1  35970  txsconn  35972  resconn  35977  cvmcn  35993  cvmsuni  36000  cvmsdisj  36001  cvmshmeo  36002  cvmlift2lem8  36041  cvmlift2lem13  36046  cvmliftphtlem  36048  cvmliftpht  36049  cvmlift3lem6  36055  msrf  36273  elmsta  36279  mthmpps  36313  mclsppslem  36314  ivthALT  37090  weiunfrlem  37219  weiunfr  37222  relowlssretop  38251  ibladdnc  38560  iblabsnclem  38566  ftc2nc  38585  dvasin  38587  isbndx  38681  isbnd3  38683  prdsbnd  38692  heiborlem3  38712  iccbnd  38739  rngohomadd  38868  rngohommul  38869  idladdcl  38918  idllmulcl  38919  idlrmulcl  38920  maxidlmax  38942  pridlc  38970  eqvreltr  39588  lshpnelb  40006  lshpcmp  40010  oplecon3  40221  opnoncon  40230  hlcvl  40381  dochshpncl  42406  lclkrslem1  42559  lclkrslem2  42560  fzne2d  42995  primrootsunit1  43112  primrootscoprmpow  43114  primrootlekpowne0  43120  aks6d1c1p1  43122  aks6d1c2  43145  sticksstones3  43163  aks5lem1  43201  aks5lem2  43202  aks5lem3a  43204  acongrep  43937  ntrneinex  45033  neicvgmex  45073  gneispace0nelrn  45096  cvgdvgrat  45253  binomcxplemdvbinom  45293  eliocre  46462  iccshift  46471  iccsuble  46472  icoiccdif  46477  mullimc  46569  limccog  46573  limciccioolb  46574  mullimcf  46576  limcperiod  46581  lptioo2  46584  lptioo1  46585  neglimc  46598  addlimc  46599  0ellimcdiv  46600  reclimc  46604  xlimmnfvlem1  46783  xlimpnfvlem1  46787  icccncfext  46838  cncfioobdlem  46847  ditgeqiooicc  46911  iblspltprt  46924  iblcncfioo  46929  itgiccshift  46931  itgperiod  46932  itgsbtaddcnst  46933  stoweidlem11  46962  stoweidlem31  46982  stoweidlem36  46987  stoweidlem38  46989  stoweidlem62  47013  dirkercncflem1  47054  dirkercncflem4  47057  fourierdlem26  47084  fourierdlem32  47090  fourierdlem33  47091  fourierdlem37  47095  fourierdlem42  47100  fourierdlem54  47111  fourierdlem63  47120  fourierdlem64  47121  fourierdlem65  47122  fourierdlem74  47131  fourierdlem75  47132  fourierdlem79  47136  fourierdlem81  47138  fourierdlem82  47139  fourierdlem89  47146  fourierdlem90  47147  fourierdlem91  47148  fourierdlem93  47150  fourierdlem101  47158  fourierdlem107  47164  fourierdlem109  47166  fourierdlem111  47168  salunicl  47267  saluncl  47268  hoidmv1lelem1  47542  hoidmv1lelem3  47544  hoidmvlelem1  47546  ovolval3  47598  iinhoiicclem  47624  smfpreimalt  47682  smfpreimaltf  47687  smfpreimale  47705  issmfgt  47707  smfpreimagt  47713  smfpreimage  47733  sigardiv  47812  sigarcol  47815  sharhght  47816  sigaradd  47817  cevathlem1  47818  cevathlem2  47819  cevath  47820  proththd  48640  perfectALTVlem2  48761  gpgnbgrvtx0  49113  gpgnbgrvtx1  49114  imasubc2  50201  imaf1co  50204  idfullsubc  50210  fucofulem1  50359  rr3fv3cld  50890