Theorem simp3d 1135

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simp3bi  1138  f1dom3fv3dif  6799  f1dom3el3dif  6800  oeeui  7968  resixp  8231  domssex2  8410  cantnflem1c  8883  cantnflem1  8885  cantnflem3  8887  cantnflem4  8888  fpwwe2lem7  9795  canthnumlem  9807  canthp1lem2  9812  wununi  9865  wunpw  9866  wunpr  9868  lelttrdi  10540  ixxdisj  12506  ixxun  12507  ixxss1  12509  ixxss2  12510  ixxss12  12511  ixxub  12512  ixxlb  12513  lbioo  12522  elicore  12542  iccsupr  12583  icodisj  12616  xov1plusxeqvd  12639  intfracq  12981  fldiv  12982  seqf1olem2  13163  cjmul  14293  icco1  14683  sumtp  14889  rpnnen2lem10  15360  ruclem2  15369  ruclem3  15370  ruclem9  15375  ruclem12  15378  dvdslegcd  15636  crth  15891  eulerthlem1  15894  eulerthlem2  15895  pcpremul  15956  prmreclem2  16029  prmreclem3  16030  4sqlem13  16069  sectcan  16804  sectco  16805  sectmon  16831  monsect  16832  funcid  16919  funcco  16920  funcsect  16921  invfuc  17023  fuciso  17024  coapm  17110  catciso  17146  postr  17343  ipodrsima  17555  psref2  17594  psasym  17600  mhm0  17733  submcl  17743  submmnd  17744  eqger  18032  eqgcpbl  18036  gaorber  18128  orbsta  18133  cayleyth  18222  pmtrrn2  18267  pmtrfinv  18268  pmtrfmvdn0  18269  dfod2  18369  sylow2blem1  18423  sylow2blem3  18425  dprdcntz  18798  dprddisj  18799  dprdffsupp  18804  dpjdisj  18843  ablfac1a  18859  ablfac1b  18860  lmodvsdir  19283  lmhmlin  19434  lbsind  19479  2idlcpbl  19635  assasca  19722  mpfind  19936  mdetunilem2  20828  mdetunilem5  20831  mdetunilem6  20832  mnfnei  21437  cnprcl  21461  lmcvg  21478  lmff  21517  lmcls  21518  lmcnp  21520  fbasssin  22052  flimfil  22185  tgpconncomp  22328  tlmtrg  22405  ustssel  22421  ustincl  22423  ustdiag  22424  ustinvel  22425  ustexhalf  22426  ustfilxp  22428  tustopn  22487  tususp  22488  imasdsf1olem  22590  xmeter  22650  xmetresbl  22654  tmstopn  22702  metustexhalf  22773  nlmnrg  22895  qdensere  22985  blcvx  23013  tgqioo  23015  icccmplem1  23037  icccmplem2  23038  reconnlem1  23041  cnmpt2pc  23139  iccpnfcnv  23155  phtpcer  23206  phtpcco2  23210  pcohtpy  23231  pcorev2  23239  pcophtb  23240  om1addcl  23244  pi1blem  23250  pi1cpbl  23255  pi1grplem  23260  pi1inv  23263  pi1xfrf  23264  pi1xfr  23266  pi1xfrcnvlem  23267  pi1cof  23270  pi1coghm  23272  cphreccllem  23389  cphsca  23390  cphsubrg  23391  cphsqrtcl2  23397  phclm  23442  tcphcph  23447  lmmcvg  23471  cmetcaulem  23498  lmcau  23523  bcthlem3  23536  bcthlem4  23537  minveclem4c  23635  minveclem2  23636  minveclem3b  23638  minveclem4  23642  minveclem6  23644  ivthicc  23666  ovollb2lem  23696  ovolshftlem1  23717  ovolscalem1  23721  ovolicc1  23724  ovolicc2lem2  23726  ovolicc2lem3  23727  ovolicc2lem4  23728  ovolicc2lem5  23729  ioombl1lem1  23766  dyadmaxlem  23805  volivth  23815  vitalilem2  23817  vitalilem4  23819  i1fima2  23887  itg2monolem1  23958  itgcnlem  23997  itgrevallem1  24002  itgreval  24004  itgle  24017  ibladd  24028  iblabslem  24035  itgspliticc  24044  itgsplitioo  24045  ditgcl  24063  ditgswap  24064  ditgsplitlem  24065  limcdif  24081  limcresi  24090  limcres  24091  limccnp  24096  limccnp2  24097  limcun  24100  dvlip  24197  dvlip2  24199  dveq0  24204  dvgt0lem1  24206  dvivthlem1  24212  dvcnvrelem1  24221  dvcnvre  24223  dvfsumlem2  24231  ftc1lem1  24239  ftc1lem2  24240  ftc1a  24241  ftc1lem4  24243  ftc2  24248  ftc2ditglem  24249  itgsubstlem  24252  ply1rem  24364  fta1glem2  24367  ig1pdvds  24377  plyrem  24501  fta1lem  24503  vieta1lem2  24507  aaliou3lem3  24540  pserulm  24617  psercnlem2  24619  psercnlem1  24620  psercn  24621  pserdvlem1  24622  pserdvlem2  24623  abelth2  24637  coseq00topi  24696  coseq0negpitopi  24697  cosordlem  24719  tanord1  24725  efif1olem1  24730  dvloglem  24835  efopnlem1  24843  logreclem  24944  relogbval  24954  nnlogbexp  24963  logbrec  24964  chordthmlem4  25017  quart1  25038  quartlem2  25040  quartlem3  25041  quart  25043  acosbnd  25082  atancj  25092  atanlogsublem  25097  atantan  25105  atanbndlem  25107  atans2  25113  dvatan  25117  atantayl  25119  divsqrtsumlem  25162  ftalem5  25259  basellem5  25267  ppisval  25286  chtleppi  25391  chpchtsum  25400  chpub  25401  mersenne  25408  perfectlem2  25411  dchrinv  25442  rplogsumlem2  25630  chpdifbndlem1  25698  pntibndlem2  25736  pntlema  25741  pntlemb  25742  pntlemg  25743  pntlemh  25744  pntlemr  25747  pntlemj  25748  pntlemf  25750  pntlemk  25751  pntlemo  25752  pntlemp  25755  pntleml  25756  abvcxp  25760  ostth2lem2  25779  axtgcont1  25823  cgr3simp3  25877  legso  25954  hlln  25962  hltr  25965  btwnhl  25969  mirhl  26034  mirbtwnhl  26035  opphllem4  26102  opphl  26106  hlpasch  26108  cgracgr  26170  cgraswap  26172  cgrahl  26179  cgracol  26180  inagswap  26194  inagne3  26197  dfcgrg2  26216  umgrnloopv  26458  umgredgne  26498  usgrnloopvALT  26551  frusgrnn0  26923  cusgrm1rusgr  26934  upgrclwlkcompim  27137  2wlkdlem6  27315  2wlkond  27321  2trlond  27323  numclwwlk2lem1  27808  numclwlk2lem2f1o  27811  numclwlk2lem2f1oOLD  27814  tncp  27909  grpolidinv  27932  nvs  28094  nvz  28100  nvtri  28101  sspn  28167  minvecolem2  28307  minvecolem4c  28311  minvecolem4  28312  minvecolem5  28313  minvecolem6  28314  adj1  29368  eliccelico  30107  elicoelioo  30108  slmdvsdir  30335  slmd0vs  30343  pmtrto1cl  30451  locfinreflem  30509  cnre2csqlem  30558  sigaclci  30797  unelsiga  30799  insiga  30802  unelldsys  30823  ldsysgenld  30825  sigapildsys  30827  ldgenpisyslem1  30828  measvun  30874  cntmeas  30891  sibfima  31002  signstfveq0  31259  signstfveq0OLD  31260  tg5segofs  31357  bnj1018  31635  subfacp1lem3  31767  subfacp1lem4  31768  subfacp1lem5  31769  sconnpht2  31823  sconnpi1  31824  txsconn  31826  resconn  31831  cvmcn  31847  cvmsuni  31854  cvmsdisj  31855  cvmshmeo  31856  cvmlift2lem8  31895  cvmlift2lem13  31900  cvmliftphtlem  31902  cvmliftpht  31903  cvmlift3lem6  31909  msrf  32042  elmsta  32048  mthmpps  32082  mclsppslem  32083  scutun12  32510  slerec  32516  ivthALT  32922  relowlssretop  33809  ibladdnc  34097  iblabsnclem  34103  ftc2nc  34124  dvasin  34126  isbndx  34210  isbnd3  34212  prdsbnd  34221  heiborlem3  34241  iccbnd  34268  rngohomadd  34397  rngohommul  34398  idladdcl  34447  idllmulcl  34448  idlrmulcl  34449  maxidlmax  34471  pridlc  34499  eqvreltr  34982  lshpnelb  35143  lshpcmp  35147  oplecon3  35358  opnoncon  35367  hlcvl  35518  dochshpncl  37543  lclkrslem1  37696  lclkrslem2  37697  acongrep  38516  ntrneinex  39341  neicvgmex  39381  gneispace0nelrn  39404  cvgdvgrat  39478  binomcxplemdvbinom  39518  eliocre  40654  iccshift  40663  iccsuble  40664  icoiccdif  40669  mullimc  40766  limccog  40770  limciccioolb  40771  mullimcf  40773  limcperiod  40778  lptioo2  40781  lptioo1  40782  neglimc  40797  addlimc  40798  0ellimcdiv  40799  reclimc  40803  xlimmnfvlem1  40982  xlimpnfvlem1  40986  icccncfext  41038  cncfioobdlem  41047  ditgeqiooicc  41113  iblspltprt  41126  iblcncfioo  41131  itgiccshift  41133  itgperiod  41134  itgsbtaddcnst  41135  stoweidlem11  41165  stoweidlem31  41185  stoweidlem36  41190  stoweidlem38  41192  stoweidlem62  41216  dirkercncflem1  41257  dirkercncflem4  41260  fourierdlem26  41287  fourierdlem32  41293  fourierdlem33  41294  fourierdlem37  41298  fourierdlem42  41303  fourierdlem54  41314  fourierdlem63  41323  fourierdlem64  41324  fourierdlem65  41325  fourierdlem74  41334  fourierdlem75  41335  fourierdlem79  41339  fourierdlem81  41341  fourierdlem82  41342  fourierdlem89  41349  fourierdlem90  41350  fourierdlem91  41351  fourierdlem93  41353  fourierdlem101  41361  fourierdlem107  41367  fourierdlem109  41369  fourierdlem111  41371  salunicl  41470  saluncl  41471  hoidmv1lelem1  41742  hoidmv1lelem3  41744  hoidmvlelem1  41746  ovolval3  41798  iinhoiicclem  41824  smfpreimalt  41877  smfpreimaltf  41882  smfpreimale  41900  issmfgt  41902  smfpreimagt  41907  smfpreimage  41927  sigardiv  41987  sigarcol  41990  sharhght  41991  sigaradd  41992  cevathlem1  41993  cevathlem2  41994  cevath  41995  proththd  42562  perfectALTVlem2  42666