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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp3bi  1148  f1dom3fv3dif  7267  f1dom3el3dif  7268  oeeui  8602  resixp  8927  domssex2  9137  cantnflem1c  9682  cantnflem1  9684  cantnflem3  9686  cantnflem4  9687  fpwwe2lem6  10631  canthnumlem  10643  canthp1lem2  10648  wununi  10701  wunpw  10702  wunpr  10704  lelttrdi  11376  ixxdisj  13339  ixxun  13340  ixxss1  13342  ixxss2  13343  ixxss12  13344  ixxub  13345  ixxlb  13346  lbioo  13355  elicore  13376  iccsupr  13419  icodisj  13453  xov1plusxeqvd  13475  intfracq  13824  fldiv  13825  seqf1olem2  14008  cjmul  15089  icco1  15484  sumtp  15695  rpnnen2lem10  16166  ruclem2  16175  ruclem3  16176  ruclem9  16181  ruclem12  16184  dvdslegcd  16445  crth  16711  eulerthlem1  16714  eulerthlem2  16715  pcpremul  16776  prmreclem2  16850  prmreclem3  16851  4sqlem13  16890  sectcan  17702  sectco  17703  sectmon  17729  monsect  17730  funcid  17820  funcco  17821  funcsect  17822  invfuc  17927  fuciso  17928  coapm  18021  catciso  18061  postr  18273  ipodrsima  18494  psref2  18523  psasym  18529  mhm0  18680  submcl  18693  submmnd  18694  eqger  19058  eqgcpbl  19062  gaorber  19172  orbsta  19177  cayleyth  19283  pmtrrn2  19328  pmtrfinv  19329  pmtrfmvdn0  19330  dfod2  19432  sylow2blem1  19488  sylow2blem3  19490  dprdcntz  19878  dprddisj  19879  dprdffsupp  19884  dpjdisj  19923  ablfac1a  19939  ablfac1b  19940  lmodvsdir  20496  lmhmlin  20646  lbsind  20691  2idlcpbl  20871  mpfind  21670  mdetunilem2  22115  mdetunilem5  22118  mdetunilem6  22119  mnfnei  22725  cnprcl  22749  lmcvg  22766  lmff  22805  lmcls  22806  lmcnp  22808  fbasssin  23340  flimfil  23473  tgpconncomp  23617  tlmtrg  23694  ustssel  23710  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ustfilxp  23717  tustopn  23776  tususp  23777  imasdsf1olem  23879  xmeter  23939  xmetresbl  23943  tmstopn  23994  metustexhalf  24065  nlmnrg  24196  qdensere  24286  blcvx  24314  tgqioo  24316  icccmplem1  24338  icccmplem2  24339  reconnlem1  24342  cnmpopc  24444  iccpnfcnv  24460  phtpcer  24511  phtpcco2  24515  pcohtpy  24536  pcorev2  24544  pcophtb  24545  om1addcl  24549  pi1blem  24555  pi1cpbl  24560  pi1grplem  24565  pi1inv  24568  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  pi1cof  24575  pi1coghm  24577  cphreccllem  24695  cphsca  24696  cphsubrg  24697  cphsqrtcl2  24703  phclm  24749  tcphcph  24754  lmmcvg  24778  cmetcaulem  24805  lmcau  24830  bcthlem3  24843  bcthlem4  24844  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  ivthicc  24975  ovollb2lem  25005  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ovolicc2lem2  25035  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2lem5  25038  ioombl1lem1  25075  dyadmaxlem  25114  volivth  25124  vitalilem2  25126  vitalilem4  25128  i1fima2  25196  itg2monolem1  25268  itgcnlem  25307  itgrevallem1  25312  itgreval  25314  itgle  25327  ibladd  25338  iblabslem  25345  itgspliticc  25354  itgsplitioo  25355  ditgcl  25375  ditgswap  25376  ditgsplitlem  25377  limcdif  25393  limcresi  25402  limcres  25403  limccnp  25408  limccnp2  25409  limcun  25412  dvlip  25510  dvlip2  25512  dveq0  25517  dvgt0lem1  25519  dvivthlem1  25525  dvcnvrelem1  25534  dvcnvre  25536  dvfsumlem2  25544  ftc1lem1  25552  ftc1lem2  25553  ftc1a  25554  ftc1lem4  25556  ftc2  25561  ftc2ditglem  25562  itgsubstlem  25565  ply1rem  25681  fta1glem2  25684  ig1pdvds  25694  plyrem  25818  fta1lem  25820  vieta1lem2  25824  aaliou3lem3  25857  pserulm  25934  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  abelth2  25954  coseq00topi  26012  coseq0negpitopi  26013  cosordlem  26039  tanord1  26046  efif1olem1  26051  dvloglem  26156  efopnlem1  26164  logreclem  26267  relogbval  26277  nnlogbexp  26286  logbrec  26287  chordthmlem4  26340  quart1  26361  quartlem2  26363  quartlem3  26364  quart  26366  acosbnd  26405  atancj  26415  atanlogsublem  26420  atantan  26428  atanbndlem  26430  atans2  26436  dvatan  26440  atantayl  26442  divsqrtsumlem  26484  ftalem5  26581  basellem5  26589  ppisval  26608  chtleppi  26713  chpchtsum  26722  chpub  26723  mersenne  26730  perfectlem2  26733  dchrinv  26764  rplogsumlem2  26988  chpdifbndlem1  27056  pntibndlem2  27094  pntlema  27099  pntlemb  27100  pntlemg  27101  pntlemh  27102  pntlemr  27105  pntlemj  27106  pntlemf  27108  pntlemk  27109  pntlemo  27110  pntlemp  27113  pntleml  27114  abvcxp  27118  ostth2lem2  27137  scutun12  27311  slerec  27320  cofcut2  27409  cofcutr  27411  cofcutrtime  27414  addsproplem5  27457  addsproplem6  27458  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  negsproplem4  27505  negsproplem6  27507  negscut2  27514  negsunif  27529  mulsproplem12  27583  ssltmul1  27602  ssltmul2  27603  mulsuniflem  27604  precsexlem11  27663  axtgcont1  27719  cgr3simp3  27773  legso  27850  hlln  27858  hltr  27861  btwnhl  27865  mirhl  27930  mirbtwnhl  27931  opphllem4  28001  opphl  28005  hlpasch  28007  cgracgr  28069  cgraswap  28071  cgrahl  28078  cgracol  28079  inagswap  28092  inagne3  28095  dfcgrg2  28114  umgrnloopv  28366  umgredgne  28405  usgrnloopvALT  28458  frusgrnn0  28828  cusgrm1rusgr  28839  upgrclwlkcompim  29038  2wlkdlem6  29185  2wlkond  29191  2trlond  29193  numclwwlk2lem1  29629  numclwlk2lem2f1o  29632  tncp  29731  grpolidinv  29754  nvs  29916  nvz  29922  nvtri  29923  sspn  29989  minvecolem2  30128  minvecolem4c  30132  minvecolem4  30133  minvecolem5  30134  minvecolem6  30135  adj1  31186  eliccelico  31988  elicoelioo  31989  prmdvdsbc  32022  pmtrto1cl  32258  cyc3evpm  32309  slmdvsdir  32361  slmd0vs  32369  sdrgdvcl  32397  sdrginvcl  32398  nsgqusf1olem3  32526  ghmquskerlem1  32528  prmidl  32558  prmidlc  32567  qsidomlem2  32572  qsnzr  32574  mxidlmax  32581  qsdrnglem2  32610  0ringmon1p  32636  ig1pmindeg  32671  ply1degltdimlem  32707  irngss  32751  ply1annig1p  32765  minplycl  32767  algextdeglem1  32772  locfinreflem  32820  cnre2csqlem  32890  sigaclci  33130  unelsiga  33132  insiga  33135  unelldsys  33156  ldsysgenld  33158  sigapildsys  33160  ldgenpisyslem1  33161  measvun  33207  cntmeas  33224  sibfima  33337  signstfveq0  33588  tg5segofs  33685  bnj1018g  33974  bnj1018  33975  pfxwlk  34114  revwlk  34115  spthcycl  34120  acycgrcycl  34138  subfacp1lem3  34173  subfacp1lem4  34174  subfacp1lem5  34175  sconnpht2  34229  sconnpi1  34230  txsconn  34232  resconn  34237  cvmcn  34253  cvmsuni  34260  cvmsdisj  34261  cvmshmeo  34262  cvmlift2lem8  34301  cvmlift2lem13  34306  cvmliftphtlem  34308  cvmliftpht  34309  cvmlift3lem6  34315  msrf  34533  elmsta  34539  mthmpps  34573  mclsppslem  34574  gg-dvfsumlem2  35183  ivthALT  35220  relowlssretop  36244  ibladdnc  36545  iblabsnclem  36551  ftc2nc  36570  dvasin  36572  isbndx  36650  isbnd3  36652  prdsbnd  36661  heiborlem3  36681  iccbnd  36708  rngohomadd  36837  rngohommul  36838  idladdcl  36887  idllmulcl  36888  idlrmulcl  36889  maxidlmax  36911  pridlc  36939  eqvreltr  37477  lshpnelb  37854  lshpcmp  37858  oplecon3  38069  opnoncon  38078  hlcvl  38229  dochshpncl  40255  lclkrslem1  40408  lclkrslem2  40409  fzne2d  40846  sticksstones3  40964  metakunt8  40992  metakunt20  41004  metakunt21  41005  metakunt22  41006  metakunt24  41008  metakunt25  41009  evlsval3  41131  flt4lem5f  41399  flt4lem7  41401  nna4b4nsq  41402  acongrep  41719  ntrneinex  42828  neicvgmex  42868  gneispace0nelrn  42891  cvgdvgrat  43072  binomcxplemdvbinom  43112  eliocre  44222  iccshift  44231  iccsuble  44232  icoiccdif  44237  mullimc  44332  limccog  44336  limciccioolb  44337  mullimcf  44339  limcperiod  44344  lptioo2  44347  lptioo1  44348  neglimc  44363  addlimc  44364  0ellimcdiv  44365  reclimc  44369  xlimmnfvlem1  44548  xlimpnfvlem1  44552  icccncfext  44603  cncfioobdlem  44612  ditgeqiooicc  44676  iblspltprt  44689  iblcncfioo  44694  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  stoweidlem11  44727  stoweidlem31  44747  stoweidlem36  44752  stoweidlem38  44754  stoweidlem62  44778  dirkercncflem1  44819  dirkercncflem4  44822  fourierdlem26  44849  fourierdlem32  44855  fourierdlem33  44856  fourierdlem37  44860  fourierdlem42  44865  fourierdlem54  44876  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem74  44896  fourierdlem75  44897  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem93  44915  fourierdlem101  44923  fourierdlem107  44929  fourierdlem109  44931  fourierdlem111  44933  salunicl  45032  saluncl  45033  hoidmv1lelem1  45307  hoidmv1lelem3  45309  hoidmvlelem1  45311  ovolval3  45363  iinhoiicclem  45389  smfpreimalt  45447  smfpreimaltf  45452  smfpreimale  45470  issmfgt  45472  smfpreimagt  45478  smfpreimage  45498  sigardiv  45577  sigarcol  45580  sharhght  45581  sigaradd  45582  cevathlem1  45583  cevathlem2  45584  cevath  45585  proththd  46282  perfectALTVlem2  46390  2idlcpblrng  46766