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  7224  f1dom3el3dif  7225  oeeui  8540  resixp  8883  domssex2  9077  cantnflem1c  9608  cantnflem1  9610  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wununi  10629  wunpw  10630  wunpr  10632  lelttrdi  11307  ixxdisj  13288  ixxun  13289  ixxss1  13291  ixxss2  13292  ixxss12  13293  ixxub  13294  ixxlb  13295  lbioo  13304  elicore  13326  iccsupr  13370  icodisj  13404  xov1plusxeqvd  13426  intfracq  13791  fldiv  13792  seqf1olem2  13977  cjmul  15077  icco1  15475  sumtp  15684  rpnnen2lem10  16160  ruclem2  16169  ruclem3  16170  ruclem9  16175  ruclem12  16178  dvdslegcd  16443  prmdvdsbc  16665  crth  16717  eulerthlem1  16720  eulerthlem2  16721  pcpremul  16783  prmreclem2  16857  prmreclem3  16858  4sqlem13  16897  sectcan  17691  sectco  17692  sectmon  17718  monsect  17719  funcid  17806  funcco  17807  funcsect  17808  invfuc  17913  fuciso  17914  coapm  18007  catciso  18047  postr  18255  ipodrsima  18476  psref2  18505  psasym  18511  mhm0  18731  submcl  18749  submmnd  18750  eqger  19119  eqgcpbl  19123  ghmqusnsglem1  19221  ghmquskerlem1  19224  gaorber  19249  orbsta  19254  cayleyth  19356  pmtrrn2  19401  pmtrfinv  19402  pmtrfmvdn0  19403  dfod2  19505  sylow2blem1  19561  sylow2blem3  19563  dprdcntz  19951  dprddisj  19952  dprdffsupp  19957  dpjdisj  19996  ablfac1a  20012  ablfac1b  20013  lmodvsdir  20849  lmhmlin  20999  lbsind  21044  2idlcpblrng  21238  evlsval3  22056  mpfind  22082  mdetunilem2  22569  mdetunilem5  22572  mdetunilem6  22573  mnfnei  23177  cnprcl  23201  lmcvg  23218  lmff  23257  lmcls  23258  lmcnp  23260  fbasssin  23792  flimfil  23925  tgpconncomp  24069  tlmtrg  24146  ustssel  24162  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ustfilxp  24169  tustopn  24226  tususp  24227  imasdsf1olem  24329  xmeter  24389  xmetresbl  24393  tmstopn  24441  metustexhalf  24512  nlmnrg  24635  qdensere  24725  blcvx  24754  tgqioo  24756  icccmplem1  24779  icccmplem2  24780  reconnlem1  24783  cnmpopc  24890  iccpnfcnv  24910  phtpcer  24962  phtpcco2  24967  pcohtpy  24988  pcorev2  24996  pcophtb  24997  om1addcl  25001  pi1blem  25007  pi1cpbl  25012  pi1grplem  25017  pi1inv  25020  pi1xfrf  25021  pi1xfr  25023  pi1xfrcnvlem  25024  pi1cof  25027  pi1coghm  25029  cphreccllem  25146  cphsca  25147  cphsubrg  25148  cphsqrtcl2  25154  phclm  25200  tcphcph  25205  lmmcvg  25229  cmetcaulem  25256  lmcau  25281  bcthlem3  25294  bcthlem4  25295  minveclem4c  25393  minveclem2  25394  minveclem3b  25396  minveclem4  25400  minveclem6  25402  ivthicc  25427  ovollb2lem  25457  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem2  25487  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2lem5  25490  ioombl1lem1  25527  dyadmaxlem  25566  volivth  25576  vitalilem2  25578  vitalilem4  25580  i1fima2  25648  itg2monolem1  25719  itgcnlem  25759  itgrevallem1  25764  itgreval  25766  itgle  25779  ibladd  25790  iblabslem  25797  itgspliticc  25806  itgsplitioo  25807  ditgcl  25827  ditgswap  25828  ditgsplitlem  25829  limcdif  25845  limcresi  25854  limcres  25855  limccnp  25860  limccnp2  25861  limcun  25864  dvlip  25966  dvlip2  25968  dveq0  25973  dvgt0lem1  25975  dvivthlem1  25981  dvcnvrelem1  25990  dvcnvre  25992  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1lem1  26010  ftc1lem2  26011  ftc1a  26012  ftc1lem4  26014  ftc2  26019  ftc2ditglem  26020  itgsubstlem  26023  ply1rem  26139  fta1glem2  26142  ig1pdvds  26153  plyrem  26281  fta1lem  26283  vieta1lem2  26287  aaliou3lem3  26320  pserulm  26399  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  abelth2  26420  coseq00topi  26479  coseq0negpitopi  26480  cosordlem  26507  tanord1  26514  efif1olem1  26519  dvloglem  26625  efopnlem1  26633  logreclem  26740  relogbval  26750  nnlogbexp  26759  logbrec  26760  chordthmlem4  26813  quart1  26834  quartlem2  26836  quartlem3  26837  quart  26839  acosbnd  26878  atancj  26888  atanlogsublem  26893  atantan  26901  atanbndlem  26903  atans2  26909  dvatan  26913  atantayl  26915  divsqrtsumlem  26958  ftalem5  27055  basellem5  27063  ppisval  27082  chtleppi  27189  chpchtsum  27198  chpub  27199  mersenne  27206  perfectlem2  27209  dchrinv  27240  rplogsumlem2  27464  chpdifbndlem1  27532  pntibndlem2  27570  pntlema  27575  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntlemp  27589  pntleml  27590  abvcxp  27594  ostth2lem2  27613  cutsun12  27798  lesrec  27807  eqcuts3  27812  cofcut2  27930  cofcutr  27932  cofcutrtime  27935  cutmax  27942  cutmin  27943  addsproplem5  27981  addsproplem6  27982  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  negsproplem4  28039  negsproplem6  28041  negcut2  28048  negsunif  28063  mulsproplem12  28135  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  precsexlem11  28225  twocut  28431  pw2cut2  28470  axtgcont1  28552  cgr3simp3  28606  legso  28683  hlln  28691  hltr  28694  btwnhl  28698  mirhl  28763  mirbtwnhl  28764  opphllem4  28834  opphl  28838  hlpasch  28840  cgracgr  28902  cgraswap  28904  cgrahl  28911  cgracol  28912  inagswap  28925  inagne3  28928  dfcgrg2  28947  umgrnloopv  29191  umgredgne  29230  usgrnloopvALT  29286  frusgrnn0  29657  cusgrm1rusgr  29668  upgrclwlkcompim  29866  2wlkdlem6  30016  2wlkond  30022  2trlond  30024  numclwwlk2lem1  30463  numclwlk2lem2f1o  30466  tncp  30565  grpolidinv  30588  nvs  30750  nvz  30756  nvtri  30757  sspn  30823  minvecolem2  30962  minvecolem4c  30966  minvecolem4  30967  minvecolem5  30968  minvecolem6  30969  adj1  32020  eliccelico  32867  elicoelioo  32868  pmtrto1cl  33192  cyc3evpm  33243  slmdvsdir  33309  slmd0vs  33317  sdrgdvcl  33392  sdrginvcl  33393  nsgqusf1olem3  33507  prmidl  33532  prmidlc  33540  qsidomlem2  33545  qsnzr  33547  mxidlmax  33557  qsdrnglem2  33588  0ringmon1p  33649  ig1pmindeg  33694  ply1degltdimlem  33799  irngss  33864  ply1annig1p  33881  minplycl  33883  algextdeglem3  33896  algextdeglem4  33897  constrsqrtcl  33956  locfinreflem  34017  cnre2csqlem  34087  sigaclci  34309  unelsiga  34311  insiga  34314  unelldsys  34335  ldsysgenld  34337  sigapildsys  34339  ldgenpisyslem1  34340  measvun  34386  cntmeas  34403  sibfima  34515  signstfveq0  34754  tg5segofs  34850  bnj1018g  35138  bnj1018  35139  pfxwlk  35337  revwlk  35338  spthcycl  35342  acycgrcycl  35360  subfacp1lem3  35395  subfacp1lem4  35396  subfacp1lem5  35397  sconnpht2  35451  sconnpi1  35452  txsconn  35454  resconn  35459  cvmcn  35475  cvmsuni  35482  cvmsdisj  35483  cvmshmeo  35484  cvmlift2lem8  35523  cvmlift2lem13  35528  cvmliftphtlem  35530  cvmliftpht  35531  cvmlift3lem6  35537  msrf  35755  elmsta  35761  mthmpps  35795  mclsppslem  35796  ivthALT  36548  weiunfrlem  36677  weiunfr  36680  relowlssretop  37607  ibladdnc  37917  iblabsnclem  37923  ftc2nc  37942  dvasin  37944  isbndx  38022  isbnd3  38024  prdsbnd  38033  heiborlem3  38053  iccbnd  38080  rngohomadd  38209  rngohommul  38210  idladdcl  38259  idllmulcl  38260  idlrmulcl  38261  maxidlmax  38283  pridlc  38311  eqvreltr  38931  lshpnelb  39349  lshpcmp  39353  oplecon3  39564  opnoncon  39573  hlcvl  39724  dochshpncl  41749  lclkrslem1  41902  lclkrslem2  41903  fzne2d  42339  primrootsunit1  42456  primrootscoprmpow  42458  primrootlekpowne0  42464  aks6d1c1p1  42466  aks6d1c2  42489  sticksstones3  42507  aks5lem1  42545  aks5lem2  42546  aks5lem3a  42548  flt4lem5f  43004  flt4lem7  43006  nna4b4nsq  43007  acongrep  43326  ntrneinex  44422  neicvgmex  44462  gneispace0nelrn  44485  cvgdvgrat  44658  binomcxplemdvbinom  44698  eliocre  45858  iccshift  45867  iccsuble  45868  icoiccdif  45873  mullimc  45965  limccog  45969  limciccioolb  45970  mullimcf  45972  limcperiod  45977  lptioo2  45980  lptioo1  45981  neglimc  45994  addlimc  45995  0ellimcdiv  45996  reclimc  46000  xlimmnfvlem1  46179  xlimpnfvlem1  46183  icccncfext  46234  cncfioobdlem  46243  ditgeqiooicc  46307  iblspltprt  46320  iblcncfioo  46325  itgiccshift  46327  itgperiod  46328  itgsbtaddcnst  46329  stoweidlem11  46358  stoweidlem31  46378  stoweidlem36  46383  stoweidlem38  46385  stoweidlem62  46409  dirkercncflem1  46450  dirkercncflem4  46453  fourierdlem26  46480  fourierdlem32  46486  fourierdlem33  46487  fourierdlem37  46491  fourierdlem42  46496  fourierdlem54  46507  fourierdlem63  46516  fourierdlem64  46517  fourierdlem65  46518  fourierdlem74  46527  fourierdlem75  46528  fourierdlem79  46532  fourierdlem81  46534  fourierdlem82  46535  fourierdlem89  46542  fourierdlem90  46543  fourierdlem91  46544  fourierdlem93  46546  fourierdlem101  46554  fourierdlem107  46560  fourierdlem109  46562  fourierdlem111  46564  salunicl  46663  saluncl  46664  hoidmv1lelem1  46938  hoidmv1lelem3  46940  hoidmvlelem1  46942  ovolval3  46994  iinhoiicclem  47020  smfpreimalt  47078  smfpreimaltf  47083  smfpreimale  47101  issmfgt  47103  smfpreimagt  47109  smfpreimage  47129  sigardiv  47208  sigarcol  47211  sharhght  47212  sigaradd  47213  cevathlem1  47214  cevathlem2  47215  cevath  47216  proththd  47963  perfectALTVlem2  48071  gpgnbgrvtx0  48423  gpgnbgrvtx1  48424  imasubc2  49500  imaf1co  49503  idfullsubc  49509  fucofulem1  49658