Theorem simp3d 1145

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp3bi  1148  f1dom3fv3dif  7223  f1dom3el3dif  7224  oeeui  8538  resixp  8881  domssex2  9075  cantnflem1c  9608  cantnflem1  9610  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wununi  10629  wunpw  10630  wunpr  10632  lelttrdi  11308  ixxdisj  13313  ixxun  13314  ixxss1  13316  ixxss2  13317  ixxss12  13318  ixxub  13319  ixxlb  13320  lbioo  13329  elicore  13351  iccsupr  13395  icodisj  13429  xov1plusxeqvd  13451  intfracq  13818  fldiv  13819  seqf1olem2  14004  cjmul  15104  icco1  15502  sumtp  15711  rpnnen2lem10  16190  ruclem2  16199  ruclem3  16200  ruclem9  16205  ruclem12  16208  dvdslegcd  16473  prmdvdsbc  16696  crth  16748  eulerthlem1  16751  eulerthlem2  16752  pcpremul  16814  prmreclem2  16888  prmreclem3  16889  4sqlem13  16928  sectcan  17722  sectco  17723  sectmon  17749  monsect  17750  funcid  17837  funcco  17838  funcsect  17839  invfuc  17944  fuciso  17945  coapm  18038  catciso  18078  postr  18286  ipodrsima  18507  psref2  18536  psasym  18542  mhm0  18762  submcl  18780  submmnd  18781  eqger  19153  eqgcpbl  19157  ghmqusnsglem1  19255  ghmquskerlem1  19258  gaorber  19283  orbsta  19288  cayleyth  19390  pmtrrn2  19435  pmtrfinv  19436  pmtrfmvdn0  19437  dfod2  19539  sylow2blem1  19595  sylow2blem3  19597  dprdcntz  19985  dprddisj  19986  dprdffsupp  19991  dpjdisj  20030  ablfac1a  20046  ablfac1b  20047  lmodvsdir  20881  lmhmlin  21030  lbsind  21075  2idlcpblrng  21269  evlsval3  22067  mpfind  22093  mdetunilem2  22578  mdetunilem5  22581  mdetunilem6  22582  mnfnei  23186  cnprcl  23210  lmcvg  23227  lmff  23266  lmcls  23267  lmcnp  23269  fbasssin  23801  flimfil  23934  tgpconncomp  24078  tlmtrg  24155  ustssel  24171  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ustfilxp  24178  tustopn  24235  tususp  24236  imasdsf1olem  24338  xmeter  24398  xmetresbl  24402  tmstopn  24450  metustexhalf  24521  nlmnrg  24644  qdensere  24734  blcvx  24763  tgqioo  24765  icccmplem1  24788  icccmplem2  24789  reconnlem1  24792  cnmpopc  24895  iccpnfcnv  24911  phtpcer  24962  phtpcco2  24966  pcohtpy  24987  pcorev2  24995  pcophtb  24996  om1addcl  25000  pi1blem  25006  pi1cpbl  25011  pi1grplem  25016  pi1inv  25019  pi1xfrf  25020  pi1xfr  25022  pi1xfrcnvlem  25023  pi1cof  25026  pi1coghm  25028  cphreccllem  25145  cphsca  25146  cphsubrg  25147  cphsqrtcl2  25153  phclm  25199  tcphcph  25204  lmmcvg  25228  cmetcaulem  25255  lmcau  25280  bcthlem3  25293  bcthlem4  25294  minveclem4c  25392  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  ivthicc  25425  ovollb2lem  25455  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem2  25485  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  ioombl1lem1  25525  dyadmaxlem  25564  volivth  25574  vitalilem2  25576  vitalilem4  25578  i1fima2  25646  itg2monolem1  25717  itgcnlem  25757  itgrevallem1  25762  itgreval  25764  itgle  25777  ibladd  25788  iblabslem  25795  itgspliticc  25804  itgsplitioo  25805  ditgcl  25825  ditgswap  25826  ditgsplitlem  25827  limcdif  25843  limcresi  25852  limcres  25853  limccnp  25858  limccnp2  25859  limcun  25862  dvlip  25960  dvlip2  25962  dveq0  25967  dvgt0lem1  25969  dvivthlem1  25975  dvcnvrelem1  25984  dvcnvre  25986  dvfsumlem2  25994  ftc1lem1  26002  ftc1lem2  26003  ftc1a  26004  ftc1lem4  26006  ftc2  26011  ftc2ditglem  26012  itgsubstlem  26015  ply1rem  26131  fta1glem2  26134  ig1pdvds  26145  plyrem  26271  fta1lem  26273  vieta1lem2  26277  aaliou3lem3  26310  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  abelth2  26407  coseq00topi  26466  coseq0negpitopi  26467  cosordlem  26494  tanord1  26501  efif1olem1  26506  dvloglem  26612  efopnlem1  26620  logreclem  26726  relogbval  26736  nnlogbexp  26745  logbrec  26746  chordthmlem4  26799  quart1  26820  quartlem2  26822  quartlem3  26823  quart  26825  acosbnd  26864  atancj  26874  atanlogsublem  26879  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  divsqrtsumlem  26943  ftalem5  27040  basellem5  27048  ppisval  27067  chtleppi  27173  chpchtsum  27182  chpub  27183  mersenne  27190  perfectlem2  27193  dchrinv  27224  rplogsumlem2  27448  chpdifbndlem1  27516  pntibndlem2  27554  pntlema  27559  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntlemp  27573  pntleml  27574  abvcxp  27578  ostth2lem2  27597  cutsun12  27782  lesrec  27791  eqcuts3  27796  cofcut2  27914  cofcutr  27916  cofcutrtime  27919  cutmax  27926  cutmin  27927  addsproplem5  27965  addsproplem6  27966  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  negsproplem4  28023  negsproplem6  28025  negcut2  28032  negsunif  28047  mulsproplem12  28119  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  precsexlem11  28209  twocut  28415  pw2cut2  28454  axtgcont1  28536  cgr3simp3  28590  legso  28667  hlln  28675  hltr  28678  btwnhl  28682  mirhl  28747  mirbtwnhl  28748  opphllem4  28818  opphl  28822  hlpasch  28824  cgracgr  28886  cgraswap  28888  cgrahl  28895  cgracol  28896  inagswap  28909  inagne3  28912  dfcgrg2  28931  umgrnloopv  29175  umgredgne  29214  usgrnloopvALT  29270  frusgrnn0  29640  cusgrm1rusgr  29651  upgrclwlkcompim  29849  2wlkdlem6  29999  2wlkond  30005  2trlond  30007  numclwwlk2lem1  30446  numclwlk2lem2f1o  30449  tncp  30549  grpolidinv  30572  nvs  30734  nvz  30740  nvtri  30741  sspn  30807  minvecolem2  30946  minvecolem4c  30950  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  adj1  32004  eliccelico  32850  elicoelioo  32851  pmtrto1cl  33160  cyc3evpm  33211  slmdvsdir  33277  slmd0vs  33285  sdrgdvcl  33360  sdrginvcl  33361  nsgqusf1olem3  33475  prmidl  33500  prmidlc  33508  qsidomlem2  33513  qsnzr  33515  mxidlmax  33525  qsdrnglem2  33556  0ringmon1p  33617  ig1pmindeg  33662  ply1degltdimlem  33766  irngss  33831  ply1annig1p  33848  minplycl  33850  algextdeglem3  33863  algextdeglem4  33864  constrsqrtcl  33923  locfinreflem  33984  cnre2csqlem  34054  sigaclci  34276  unelsiga  34278  insiga  34281  unelldsys  34302  ldsysgenld  34304  sigapildsys  34306  ldgenpisyslem1  34307  measvun  34353  cntmeas  34370  sibfima  34482  signstfveq0  34721  tg5segofs  34817  bnj1018g  35105  bnj1018  35106  pfxwlk  35306  revwlk  35307  spthcycl  35311  acycgrcycl  35329  subfacp1lem3  35364  subfacp1lem4  35365  subfacp1lem5  35366  sconnpht2  35420  sconnpi1  35421  txsconn  35423  resconn  35428  cvmcn  35444  cvmsuni  35451  cvmsdisj  35452  cvmshmeo  35453  cvmlift2lem8  35492  cvmlift2lem13  35497  cvmliftphtlem  35499  cvmliftpht  35500  cvmlift3lem6  35506  msrf  35724  elmsta  35730  mthmpps  35764  mclsppslem  35765  ivthALT  36517  weiunfrlem  36646  weiunfr  36649  relowlssretop  37679  ibladdnc  37998  iblabsnclem  38004  ftc2nc  38023  dvasin  38025  isbndx  38103  isbnd3  38105  prdsbnd  38114  heiborlem3  38134  iccbnd  38161  rngohomadd  38290  rngohommul  38291  idladdcl  38340  idllmulcl  38341  idlrmulcl  38342  maxidlmax  38364  pridlc  38392  eqvreltr  39012  lshpnelb  39430  lshpcmp  39434  oplecon3  39645  opnoncon  39654  hlcvl  39805  dochshpncl  41830  lclkrslem1  41983  lclkrslem2  41984  fzne2d  42419  primrootsunit1  42536  primrootscoprmpow  42538  primrootlekpowne0  42544  aks6d1c1p1  42546  aks6d1c2  42569  sticksstones3  42587  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  flt4lem5f  43090  flt4lem7  43092  nna4b4nsq  43093  acongrep  43408  ntrneinex  44504  neicvgmex  44544  gneispace0nelrn  44567  cvgdvgrat  44740  binomcxplemdvbinom  44780  eliocre  45939  iccshift  45948  iccsuble  45949  icoiccdif  45954  mullimc  46046  limccog  46050  limciccioolb  46051  mullimcf  46053  limcperiod  46058  lptioo2  46061  lptioo1  46062  neglimc  46075  addlimc  46076  0ellimcdiv  46077  reclimc  46081  xlimmnfvlem1  46260  xlimpnfvlem1  46264  icccncfext  46315  cncfioobdlem  46324  ditgeqiooicc  46388  iblspltprt  46401  iblcncfioo  46406  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem11  46439  stoweidlem31  46459  stoweidlem36  46464  stoweidlem38  46466  stoweidlem62  46490  dirkercncflem1  46531  dirkercncflem4  46534  fourierdlem26  46561  fourierdlem32  46567  fourierdlem33  46568  fourierdlem37  46572  fourierdlem42  46577  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem93  46627  fourierdlem101  46635  fourierdlem107  46641  fourierdlem109  46643  fourierdlem111  46645  salunicl  46744  saluncl  46745  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmvlelem1  47023  ovolval3  47075  iinhoiicclem  47101  smfpreimalt  47159  smfpreimaltf  47164  smfpreimale  47182  issmfgt  47184  smfpreimagt  47190  smfpreimage  47210  sigardiv  47289  sigarcol  47292  sharhght  47293  sigaradd  47294  cevathlem1  47295  cevathlem2  47296  cevath  47297  proththd  48071  perfectALTVlem2  48192  gpgnbgrvtx0  48544  gpgnbgrvtx1  48545  imasubc2  49621  imaf1co  49624  idfullsubc  49630  fucofulem1  49779