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  7288  f1dom3el3dif  7289  oeeui  8640  resixp  8973  domssex2  9177  cantnflem1c  9727  cantnflem1  9729  cantnflem3  9731  cantnflem4  9732  fpwwe2lem6  10676  canthnumlem  10688  canthp1lem2  10693  wununi  10746  wunpw  10747  wunpr  10749  lelttrdi  11423  ixxdisj  13402  ixxun  13403  ixxss1  13405  ixxss2  13406  ixxss12  13407  ixxub  13408  ixxlb  13409  lbioo  13418  elicore  13439  iccsupr  13482  icodisj  13516  xov1plusxeqvd  13538  intfracq  13899  fldiv  13900  seqf1olem2  14083  cjmul  15181  icco1  15576  sumtp  15785  rpnnen2lem10  16259  ruclem2  16268  ruclem3  16269  ruclem9  16274  ruclem12  16277  dvdslegcd  16541  prmdvdsbc  16763  crth  16815  eulerthlem1  16818  eulerthlem2  16819  pcpremul  16881  prmreclem2  16955  prmreclem3  16956  4sqlem13  16995  sectcan  17799  sectco  17800  sectmon  17826  monsect  17827  funcid  17915  funcco  17916  funcsect  17917  invfuc  18022  fuciso  18023  coapm  18116  catciso  18156  postr  18366  ipodrsima  18586  psref2  18615  psasym  18621  mhm0  18807  submcl  18825  submmnd  18826  eqger  19196  eqgcpbl  19200  ghmqusnsglem1  19298  ghmquskerlem1  19301  gaorber  19326  orbsta  19331  cayleyth  19433  pmtrrn2  19478  pmtrfinv  19479  pmtrfmvdn0  19480  dfod2  19582  sylow2blem1  19638  sylow2blem3  19640  dprdcntz  20028  dprddisj  20029  dprdffsupp  20034  dpjdisj  20073  ablfac1a  20089  ablfac1b  20090  lmodvsdir  20884  lmhmlin  21034  lbsind  21079  2idlcpblrng  21281  mpfind  22131  mdetunilem2  22619  mdetunilem5  22622  mdetunilem6  22623  mnfnei  23229  cnprcl  23253  lmcvg  23270  lmff  23309  lmcls  23310  lmcnp  23312  fbasssin  23844  flimfil  23977  tgpconncomp  24121  tlmtrg  24198  ustssel  24214  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ustfilxp  24221  tustopn  24280  tususp  24281  imasdsf1olem  24383  xmeter  24443  xmetresbl  24447  tmstopn  24498  metustexhalf  24569  nlmnrg  24700  qdensere  24790  blcvx  24819  tgqioo  24821  icccmplem1  24844  icccmplem2  24845  reconnlem1  24848  cnmpopc  24955  iccpnfcnv  24975  phtpcer  25027  phtpcco2  25032  pcohtpy  25053  pcorev2  25061  pcophtb  25062  om1addcl  25066  pi1blem  25072  pi1cpbl  25077  pi1grplem  25082  pi1inv  25085  pi1xfrf  25086  pi1xfr  25088  pi1xfrcnvlem  25089  pi1cof  25092  pi1coghm  25094  cphreccllem  25212  cphsca  25213  cphsubrg  25214  cphsqrtcl2  25220  phclm  25266  tcphcph  25271  lmmcvg  25295  cmetcaulem  25322  lmcau  25347  bcthlem3  25360  bcthlem4  25361  minveclem4c  25459  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem6  25468  ivthicc  25493  ovollb2lem  25523  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem2  25553  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  ioombl1lem1  25593  dyadmaxlem  25632  volivth  25642  vitalilem2  25644  vitalilem4  25646  i1fima2  25714  itg2monolem1  25785  itgcnlem  25825  itgrevallem1  25830  itgreval  25832  itgle  25845  ibladd  25856  iblabslem  25863  itgspliticc  25872  itgsplitioo  25873  ditgcl  25893  ditgswap  25894  ditgsplitlem  25895  limcdif  25911  limcresi  25920  limcres  25921  limccnp  25926  limccnp2  25927  limcun  25930  dvlip  26032  dvlip2  26034  dveq0  26039  dvgt0lem1  26041  dvivthlem1  26047  dvcnvrelem1  26056  dvcnvre  26058  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1lem1  26076  ftc1lem2  26077  ftc1a  26078  ftc1lem4  26080  ftc2  26085  ftc2ditglem  26086  itgsubstlem  26089  ply1rem  26205  fta1glem2  26208  ig1pdvds  26219  plyrem  26347  fta1lem  26349  vieta1lem2  26353  aaliou3lem3  26386  pserulm  26465  psercnlem2  26468  psercnlem1  26469  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  abelth2  26486  coseq00topi  26544  coseq0negpitopi  26545  cosordlem  26572  tanord1  26579  efif1olem1  26584  dvloglem  26690  efopnlem1  26698  logreclem  26805  relogbval  26815  nnlogbexp  26824  logbrec  26825  chordthmlem4  26878  quart1  26899  quartlem2  26901  quartlem3  26902  quart  26904  acosbnd  26943  atancj  26953  atanlogsublem  26958  atantan  26966  atanbndlem  26968  atans2  26974  dvatan  26978  atantayl  26980  divsqrtsumlem  27023  ftalem5  27120  basellem5  27128  ppisval  27147  chtleppi  27254  chpchtsum  27263  chpub  27264  mersenne  27271  perfectlem2  27274  dchrinv  27305  rplogsumlem2  27529  chpdifbndlem1  27597  pntibndlem2  27635  pntlema  27640  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntlemp  27654  pntleml  27655  abvcxp  27659  ostth2lem2  27678  scutun12  27855  slerec  27864  cofcut2  27956  cofcutr  27958  cofcutrtime  27961  cutmax  27968  cutmin  27969  addsproplem5  28006  addsproplem6  28007  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  negsproplem4  28063  negsproplem6  28065  negscut2  28072  negsunif  28087  mulsproplem12  28153  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  precsexlem11  28241  axtgcont1  28476  cgr3simp3  28530  legso  28607  hlln  28615  hltr  28618  btwnhl  28622  mirhl  28687  mirbtwnhl  28688  opphllem4  28758  opphl  28762  hlpasch  28764  cgracgr  28826  cgraswap  28828  cgrahl  28835  cgracol  28836  inagswap  28849  inagne3  28852  dfcgrg2  28871  umgrnloopv  29123  umgredgne  29162  usgrnloopvALT  29218  frusgrnn0  29589  cusgrm1rusgr  29600  upgrclwlkcompim  29801  2wlkdlem6  29951  2wlkond  29957  2trlond  29959  numclwwlk2lem1  30395  numclwlk2lem2f1o  30398  tncp  30497  grpolidinv  30520  nvs  30682  nvz  30688  nvtri  30689  sspn  30755  minvecolem2  30894  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  adj1  31952  eliccelico  32779  elicoelioo  32780  pmtrto1cl  33119  cyc3evpm  33170  slmdvsdir  33222  slmd0vs  33230  sdrgdvcl  33301  sdrginvcl  33302  nsgqusf1olem3  33443  prmidl  33468  prmidlc  33476  qsidomlem2  33481  qsnzr  33483  mxidlmax  33493  qsdrnglem2  33524  0ringmon1p  33583  ig1pmindeg  33622  ply1degltdimlem  33673  irngss  33737  ply1annig1p  33747  minplycl  33749  algextdeglem3  33760  algextdeglem4  33761  locfinreflem  33839  cnre2csqlem  33909  sigaclci  34133  unelsiga  34135  insiga  34138  unelldsys  34159  ldsysgenld  34161  sigapildsys  34163  ldgenpisyslem1  34164  measvun  34210  cntmeas  34227  sibfima  34340  signstfveq0  34592  tg5segofs  34688  bnj1018g  34977  bnj1018  34978  pfxwlk  35129  revwlk  35130  spthcycl  35134  acycgrcycl  35152  subfacp1lem3  35187  subfacp1lem4  35188  subfacp1lem5  35189  sconnpht2  35243  sconnpi1  35244  txsconn  35246  resconn  35251  cvmcn  35267  cvmsuni  35274  cvmsdisj  35275  cvmshmeo  35276  cvmlift2lem8  35315  cvmlift2lem13  35320  cvmliftphtlem  35322  cvmliftpht  35323  cvmlift3lem6  35329  msrf  35547  elmsta  35553  mthmpps  35587  mclsppslem  35588  ivthALT  36336  weiunfrlem  36465  weiunfr  36468  relowlssretop  37364  ibladdnc  37684  iblabsnclem  37690  ftc2nc  37709  dvasin  37711  isbndx  37789  isbnd3  37791  prdsbnd  37800  heiborlem3  37820  iccbnd  37847  rngohomadd  37976  rngohommul  37977  idladdcl  38026  idllmulcl  38027  idlrmulcl  38028  maxidlmax  38050  pridlc  38078  eqvreltr  38608  lshpnelb  38985  lshpcmp  38989  oplecon3  39200  opnoncon  39209  hlcvl  39360  dochshpncl  41386  lclkrslem1  41539  lclkrslem2  41540  fzne2d  41981  primrootsunit1  42098  primrootscoprmpow  42100  primrootlekpowne0  42106  aks6d1c1p1  42108  aks6d1c2  42131  sticksstones3  42149  aks5lem1  42187  aks5lem2  42188  aks5lem3a  42190  metakunt8  42213  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt24  42229  metakunt25  42230  evlsval3  42569  flt4lem5f  42667  flt4lem7  42669  nna4b4nsq  42670  acongrep  42992  ntrneinex  44090  neicvgmex  44130  gneispace0nelrn  44153  cvgdvgrat  44332  binomcxplemdvbinom  44372  eliocre  45522  iccshift  45531  iccsuble  45532  icoiccdif  45537  mullimc  45631  limccog  45635  limciccioolb  45636  mullimcf  45638  limcperiod  45643  lptioo2  45646  lptioo1  45647  neglimc  45662  addlimc  45663  0ellimcdiv  45664  reclimc  45668  xlimmnfvlem1  45847  xlimpnfvlem1  45851  icccncfext  45902  cncfioobdlem  45911  ditgeqiooicc  45975  iblspltprt  45988  iblcncfioo  45993  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem11  46026  stoweidlem31  46046  stoweidlem36  46051  stoweidlem38  46053  stoweidlem62  46077  dirkercncflem1  46118  dirkercncflem4  46121  fourierdlem26  46148  fourierdlem32  46154  fourierdlem33  46155  fourierdlem37  46159  fourierdlem42  46164  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem93  46214  fourierdlem101  46222  fourierdlem107  46228  fourierdlem109  46230  fourierdlem111  46232  salunicl  46331  saluncl  46332  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmvlelem1  46610  ovolval3  46662  iinhoiicclem  46688  smfpreimalt  46746  smfpreimaltf  46751  smfpreimale  46769  issmfgt  46771  smfpreimagt  46777  smfpreimage  46797  sigardiv  46876  sigarcol  46879  sharhght  46880  sigaradd  46881  cevathlem1  46882  cevathlem2  46883  cevath  46884  proththd  47601  perfectALTVlem2  47709  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  fucofulem1  49005