Theorem simp3d 1143

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp3bi  1146  f1dom3fv3dif  7287  f1dom3el3dif  7288  oeeui  8638  resixp  8971  domssex2  9175  cantnflem1c  9724  cantnflem1  9726  cantnflem3  9728  cantnflem4  9729  fpwwe2lem6  10673  canthnumlem  10685  canthp1lem2  10690  wununi  10743  wunpw  10744  wunpr  10746  lelttrdi  11420  ixxdisj  13398  ixxun  13399  ixxss1  13401  ixxss2  13402  ixxss12  13403  ixxub  13404  ixxlb  13405  lbioo  13414  elicore  13435  iccsupr  13478  icodisj  13512  xov1plusxeqvd  13534  intfracq  13895  fldiv  13896  seqf1olem2  14079  cjmul  15177  icco1  15572  sumtp  15781  rpnnen2lem10  16255  ruclem2  16264  ruclem3  16265  ruclem9  16270  ruclem12  16273  dvdslegcd  16537  prmdvdsbc  16759  crth  16811  eulerthlem1  16814  eulerthlem2  16815  pcpremul  16876  prmreclem2  16950  prmreclem3  16951  4sqlem13  16990  sectcan  17802  sectco  17803  sectmon  17829  monsect  17830  funcid  17920  funcco  17921  funcsect  17922  invfuc  18030  fuciso  18031  coapm  18124  catciso  18164  postr  18377  ipodrsima  18598  psref2  18627  psasym  18633  mhm0  18819  submcl  18837  submmnd  18838  eqger  19208  eqgcpbl  19212  ghmqusnsglem1  19310  ghmquskerlem1  19313  gaorber  19338  orbsta  19343  cayleyth  19447  pmtrrn2  19492  pmtrfinv  19493  pmtrfmvdn0  19494  dfod2  19596  sylow2blem1  19652  sylow2blem3  19654  dprdcntz  20042  dprddisj  20043  dprdffsupp  20048  dpjdisj  20087  ablfac1a  20103  ablfac1b  20104  lmodvsdir  20900  lmhmlin  21051  lbsind  21096  2idlcpblrng  21298  mpfind  22148  mdetunilem2  22634  mdetunilem5  22637  mdetunilem6  22638  mnfnei  23244  cnprcl  23268  lmcvg  23285  lmff  23324  lmcls  23325  lmcnp  23327  fbasssin  23859  flimfil  23992  tgpconncomp  24136  tlmtrg  24213  ustssel  24229  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ustfilxp  24236  tustopn  24295  tususp  24296  imasdsf1olem  24398  xmeter  24458  xmetresbl  24462  tmstopn  24513  metustexhalf  24584  nlmnrg  24715  qdensere  24805  blcvx  24833  tgqioo  24835  icccmplem1  24857  icccmplem2  24858  reconnlem1  24861  cnmpopc  24968  iccpnfcnv  24988  phtpcer  25040  phtpcco2  25045  pcohtpy  25066  pcorev2  25074  pcophtb  25075  om1addcl  25079  pi1blem  25085  pi1cpbl  25090  pi1grplem  25095  pi1inv  25098  pi1xfrf  25099  pi1xfr  25101  pi1xfrcnvlem  25102  pi1cof  25105  pi1coghm  25107  cphreccllem  25225  cphsca  25226  cphsubrg  25227  cphsqrtcl2  25233  phclm  25279  tcphcph  25284  lmmcvg  25308  cmetcaulem  25335  lmcau  25360  bcthlem3  25373  bcthlem4  25374  minveclem4c  25472  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem6  25481  ivthicc  25506  ovollb2lem  25536  ovolshftlem1  25557  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  ioombl1lem1  25606  dyadmaxlem  25645  volivth  25655  vitalilem2  25657  vitalilem4  25659  i1fima2  25727  itg2monolem1  25799  itgcnlem  25839  itgrevallem1  25844  itgreval  25846  itgle  25859  ibladd  25870  iblabslem  25877  itgspliticc  25886  itgsplitioo  25887  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  limcdif  25925  limcresi  25934  limcres  25935  limccnp  25940  limccnp2  25941  limcun  25944  dvlip  26046  dvlip2  26048  dveq0  26053  dvgt0lem1  26055  dvivthlem1  26061  dvcnvrelem1  26070  dvcnvre  26072  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1lem1  26090  ftc1lem2  26091  ftc1a  26092  ftc1lem4  26094  ftc2  26099  ftc2ditglem  26100  itgsubstlem  26103  ply1rem  26219  fta1glem2  26222  ig1pdvds  26233  plyrem  26361  fta1lem  26363  vieta1lem2  26367  aaliou3lem3  26400  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  abelth2  26500  coseq00topi  26558  coseq0negpitopi  26559  cosordlem  26586  tanord1  26593  efif1olem1  26598  dvloglem  26704  efopnlem1  26712  logreclem  26819  relogbval  26829  nnlogbexp  26838  logbrec  26839  chordthmlem4  26892  quart1  26913  quartlem2  26915  quartlem3  26916  quart  26918  acosbnd  26957  atancj  26967  atanlogsublem  26972  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  divsqrtsumlem  27037  ftalem5  27134  basellem5  27142  ppisval  27161  chtleppi  27268  chpchtsum  27277  chpub  27278  mersenne  27285  perfectlem2  27288  dchrinv  27319  rplogsumlem2  27543  chpdifbndlem1  27611  pntibndlem2  27649  pntlema  27654  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemr  27660  pntlemj  27661  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntlemp  27668  pntleml  27669  abvcxp  27673  ostth2lem2  27692  scutun12  27869  slerec  27878  cofcut2  27970  cofcutr  27972  cofcutrtime  27975  cutmax  27982  cutmin  27983  addsproplem5  28020  addsproplem6  28021  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  negsproplem4  28077  negsproplem6  28079  negscut2  28086  negsunif  28101  mulsproplem12  28167  ssltmul1  28187  ssltmul2  28188  mulsuniflem  28189  precsexlem11  28255  axtgcont1  28490  cgr3simp3  28544  legso  28621  hlln  28629  hltr  28632  btwnhl  28636  mirhl  28701  mirbtwnhl  28702  opphllem4  28772  opphl  28776  hlpasch  28778  cgracgr  28840  cgraswap  28842  cgrahl  28849  cgracol  28850  inagswap  28863  inagne3  28866  dfcgrg2  28885  umgrnloopv  29137  umgredgne  29176  usgrnloopvALT  29232  frusgrnn0  29603  cusgrm1rusgr  29614  upgrclwlkcompim  29813  2wlkdlem6  29960  2wlkond  29966  2trlond  29968  numclwwlk2lem1  30404  numclwlk2lem2f1o  30407  tncp  30506  grpolidinv  30529  nvs  30691  nvz  30697  nvtri  30698  sspn  30764  minvecolem2  30903  minvecolem4c  30907  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  adj1  31961  eliccelico  32785  elicoelioo  32786  pmtrto1cl  33101  cyc3evpm  33152  slmdvsdir  33204  slmd0vs  33212  sdrgdvcl  33280  sdrginvcl  33281  nsgqusf1olem3  33422  prmidl  33447  prmidlc  33455  qsidomlem2  33460  qsnzr  33462  mxidlmax  33472  qsdrnglem2  33503  0ringmon1p  33562  ig1pmindeg  33601  ply1degltdimlem  33649  irngss  33701  ply1annig1p  33711  minplycl  33713  algextdeglem3  33724  algextdeglem4  33725  locfinreflem  33800  cnre2csqlem  33870  sigaclci  34112  unelsiga  34114  insiga  34117  unelldsys  34138  ldsysgenld  34140  sigapildsys  34142  ldgenpisyslem1  34143  measvun  34189  cntmeas  34206  sibfima  34319  signstfveq0  34570  tg5segofs  34666  bnj1018g  34955  bnj1018  34956  pfxwlk  35107  revwlk  35108  spthcycl  35113  acycgrcycl  35131  subfacp1lem3  35166  subfacp1lem4  35167  subfacp1lem5  35168  sconnpht2  35222  sconnpi1  35223  txsconn  35225  resconn  35230  cvmcn  35246  cvmsuni  35253  cvmsdisj  35254  cvmshmeo  35255  cvmlift2lem8  35294  cvmlift2lem13  35299  cvmliftphtlem  35301  cvmliftpht  35302  cvmlift3lem6  35308  msrf  35526  elmsta  35532  mthmpps  35566  mclsppslem  35567  ivthALT  36317  weiunfrlem  36446  weiunfr  36449  relowlssretop  37345  ibladdnc  37663  iblabsnclem  37669  ftc2nc  37688  dvasin  37690  isbndx  37768  isbnd3  37770  prdsbnd  37779  heiborlem3  37799  iccbnd  37826  rngohomadd  37955  rngohommul  37956  idladdcl  38005  idllmulcl  38006  idlrmulcl  38007  maxidlmax  38029  pridlc  38057  eqvreltr  38588  lshpnelb  38965  lshpcmp  38969  oplecon3  39180  opnoncon  39189  hlcvl  39340  dochshpncl  41366  lclkrslem1  41519  lclkrslem2  41520  fzne2d  41961  primrootsunit1  42078  primrootscoprmpow  42080  primrootlekpowne0  42086  aks6d1c1p1  42088  aks6d1c2  42111  sticksstones3  42129  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  metakunt8  42193  metakunt20  42205  metakunt21  42206  metakunt22  42207  metakunt24  42209  metakunt25  42210  evlsval3  42545  flt4lem5f  42643  flt4lem7  42645  nna4b4nsq  42646  acongrep  42968  ntrneinex  44066  neicvgmex  44106  gneispace0nelrn  44129  cvgdvgrat  44308  binomcxplemdvbinom  44348  eliocre  45461  iccshift  45470  iccsuble  45471  icoiccdif  45476  mullimc  45571  limccog  45575  limciccioolb  45576  mullimcf  45578  limcperiod  45583  lptioo2  45586  lptioo1  45587  neglimc  45602  addlimc  45603  0ellimcdiv  45604  reclimc  45608  xlimmnfvlem1  45787  xlimpnfvlem1  45791  icccncfext  45842  cncfioobdlem  45851  ditgeqiooicc  45915  iblspltprt  45928  iblcncfioo  45933  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem11  45966  stoweidlem31  45986  stoweidlem36  45991  stoweidlem38  45993  stoweidlem62  46017  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem26  46088  fourierdlem32  46094  fourierdlem33  46095  fourierdlem37  46099  fourierdlem42  46104  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem93  46154  fourierdlem101  46162  fourierdlem107  46168  fourierdlem109  46170  fourierdlem111  46172  salunicl  46271  saluncl  46272  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmvlelem1  46550  ovolval3  46602  iinhoiicclem  46628  smfpreimalt  46686  smfpreimaltf  46691  smfpreimale  46709  issmfgt  46711  smfpreimagt  46717  smfpreimage  46737  sigardiv  46816  sigarcol  46819  sharhght  46820  sigaradd  46821  cevathlem1  46822  cevathlem2  46823  cevath  46824  proththd  47538  perfectALTVlem2  47646  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965