Theorem simp1d 1160

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp1bi  1163  f1dom3fv3dif  7264  f1dom3el3dif  7265  f1prex  7284  oeeui  8595  oeeu  8596  domssex2  9140  domssex  9141  cantnflem1a  9670  cantnflem1b  9671  cantnflem1c  9672  cantnflem1d  9673  cantnflem1  9674  cantnflem3  9676  cantnflem4  9677  fpwwe2lem6  10702  canthnumlem  10714  canthp1lem2  10719  wuntr  10771  lelttrdi  11453  supmul1  12267  supmullem1  12268  supmullem2  12269  supmul  12270  ixxdisj  13472  ixxun  13473  ixxss1  13475  ixxss2  13476  ixxss12  13477  ixxub  13478  ixxlb  13479  iccss2  13529  iocssre  13539  icossre  13540  iccssre  13541  icodisj  13588  iccf1o  13608  xov1plusxeqvd  13610  fzen  13654  intfracq  13979  fldiv  13980  remul  15276  01sqrexlem6  15394  resqrtth  15402  sqrtth  15512  ruclem6  16383  ruclem9  16386  ruclem12  16389  gcdn0cl  16652  crth  16935  phimullem  16936  eulerthlem1  16938  eulerthlem2  16939  pcpremul  17001  prmreclem3  17076  sectcan  17910  sectco  17911  sectmon  17937  monsect  17938  funcf1  18021  funcsect  18027  invfuc  18132  coapm  18226  catciso  18266  psrel  18723  pstr  18731  mhmf  18964  submss  18984  eqger  19370  eqgcpbl  19374  gaorber  19502  orbstafun  19505  cayleyth  19609  dprdgrp  20201  dprdff  20208  ablfac1a  20265  ablfac1b  20266  lmodvscl  21133  lbsss  21332  2idlcpblrng  21545  prmidlidl  21605  evlsval3  22378  mpfind  22404  mdetunilem2  22908  mdetunilem5  22911  mdetunilem6  22912  chfacfisfcpmat  23153  cnptop1  23540  lmfpm  23593  lmff  23599  lmcnp  23602  flimtop  24264  tlmtmd  24486  ustssxp  24504  ustdiag  24508  ustfilxp  24512  ustbas2  24524  tusbas  24566  imasdsf1olem  24672  xmeter  24732  tmsbas  24782  metustexhalf  24855  nlmngp  24976  qdensere  25068  blcvx  25097  tgqioo  25099  icccmplem2  25123  reconnlem1  25126  cnmpopc  25229  icoopnst  25240  iocopnst  25241  iccpnfcnv  25245  phtpcer  25296  phtpcco2  25300  pcohtpylem  25320  pcohtpy  25321  pcopt  25323  pcopt2  25324  pcorevlem  25327  pcorev2  25329  pcophtb  25330  om1addcl  25334  pi1grplem  25350  pi1inv  25353  pi1xfrf  25354  pi1xfr  25356  pi1xfrcnvlem  25357  pi1xfrcnv  25358  pi1cof  25360  pi1coghm  25362  cphphl  25472  cphreccllem  25479  cphsqrtcl2  25487  phclm  25533  tcphcph  25538  lmcau  25614  bcthlem4  25628  minveclem4c  25726  minveclem2  25727  minveclem3b  25729  minveclem4  25733  minveclem6  25735  ivthicc  25759  ovolfsval  25771  ovollb2lem  25789  ovolshftlem1  25810  ovolscalem1  25814  ovolicc2lem2  25819  ovolicc2lem5  25822  ovolicopnf  25825  ioombl1lem1  25859  ioombl1lem3  25861  ioombl1lem4  25862  uniioovol  25880  uniioombllem2a  25883  uniioombllem2  25884  uniioombllem3a  25885  uniioombllem3  25886  uniioombllem4  25887  uniioombllem6  25889  vitalilem2  25910  vitalilem3  25911  vitalilem4  25912  i1ff  25977  itg2monolem1  26051  itgreval  26097  ibladd  26121  iblabslem  26128  itgspliticc  26137  itgsplitioo  26138  ditgcl  26158  ditgswap  26159  ditgsplitlem  26160  ditgsplit  26161  limcresi  26185  dvlip2  26295  dveq0  26300  dvcnvre  26319  dvfsumlem2  26327  ftc1a  26337  ply1rem  26464  facth1  26465  fta1glem1  26466  fta1glem2  26467  ig1pcl  26477  ig1pdvds  26478  plyrem  26608  facth  26609  vieta1lem1  26615  vieta1lem2  26616  aaliou3lem3  26653  aaliou3lem7  26658  pserulm  26731  psercnlem2  26733  psercn  26735  pserdvlem1  26736  pserdvlem2  26737  pserdv  26738  abelth2  26751  coseq00topi  26813  coseq0negpitopi  26814  cosordlem  26840  efif1olem1  26852  dvloglem  26958  loglesqrt  27071  relogbval  27082  nnlogbexp  27091  logbrec  27092  quart1  27166  quartlem2  27168  quartlem3  27169  quartlem4  27170  quart  27171  asinsinlem  27201  atanlogsublem  27225  atans2  27241  dvatan  27245  rlimcnp2  27276  divsqrtsumlem  27289  ftalem5  27386  ftalem7  27388  basellem4  27393  basellem5  27394  perfectlem2  27539  dchrinv  27570  chpdifbndlem1  27862  pntibndlem2  27900  pntlema  27905  pntlemb  27906  pntlemg  27907  pntlemh  27908  pntlemn  27909  pntlemq  27910  pntlemr  27911  pntlemj  27912  pntlemf  27914  pntlemk  27915  pntlemo  27916  pntlemp  27919  pntleml  27920  abvcxp  27924  flt4lem5f  27969  flt4lem7  27971  nna4b4nsq  27972  cutscl  28150  cutsun12  28158  ltsrec  28169  addsproplem6  28342  addsprop  28344  addscld  28348  negsproplem6  28401  negsprop  28403  mulsproplem11  28494  mulsproplem12  28495  axtgbtwnid  28910  cgr3simp1  28965  hlne1  29053  hltr  29058  btwnhl  29062  mirhl  29133  opphllem4  29208  hlpasch  29216  inagswap  29342  inagne1  29343  dfcgrg2  29390  wlkf  30177  wlk1ewlk  30202  pfxwlk  30248  revwlk  30249  subgrwlk  30251  2wlkdlem6  30502  2wlkond  30508  2trlond  30510  grpofo  31083  vcablo  31153  nvvc  31199  sspba  31311  sspg  31312  minvecolem2  31459  minvecolem4c  31463  minvecolem4  31464  minvecolem5  31465  minvecolem6  31466  eleigveccl  32543  tpssad  33117  xrofsup  33341  eliccelico  33351  elicoelioo  33352  cyc3evpm  33693  slmdvscl  33757  slmdvsass  33760  imaslmod  33896  mxidlidl  33970  0ringmon1p  34071  irngss  34301  algextdeglem1  34331  constrsqrtcl  34393  baselsiga  34729  insiga  34752  ldsysgenld  34775  sigapildsys  34777  ldgenpisyslem1  34778  measfrge0  34818  sibfmbl  34950  eulerpartlemt  34986  eulerpartlemmf  34990  probfinmeasbALTV  35044  tg5segofs  35288  subfacp1lem2a  35914  subfacp1lem2b  35915  subfacp1lem3  35916  subfacp1lem4  35917  subfacp1lem5  35918  sconnpht2  35972  sconnpi1  35973  cvxsconn  35977  cvmlift2lem3  36039  cvmlift2lem5  36041  cvmlift2lem6  36042  cvmlift2lem7  36043  cvmlift2lem12  36048  cvmliftphtlem  36051  cvmliftpht  36052  cvmlift3lem2  36054  cvmlift3lem4  36056  cvmlift3lem5  36057  cvmlift3lem6  36058  msrf  36276  elmsta  36282  mthmpps  36316  mclsppslem  36317  mclspps  36318  weiunfrlem  37222  weiunpo  37223  weiunso  37224  weiunfr  37225  weiunse  37226  iblabsnclem  38569  dvasin  38590  isbnd3  38686  heiborlem3  38715  iccbnd  38742  rngohomf  38868  idlss  38918  lshplss  40006  opoccl  40219  opococ  40220  oplecon3  40224  hloml  40382  lclkrslem1  42562  lclkrslem2  42563  dvrelog2  43082  dvrelog3  43083  aks4d1p1p5  43093  primrootsunit1  43115  primrootscoprmpow  43117  primrootscoprbij  43120  primrootspoweq0  43124  aks6d1c1p2  43127  aks6d1c1p3  43128  aks6d1c1p4  43129  aks6d1c1p5  43130  aks6d1c1p7  43131  aks6d1c1p6  43132  aks6d1c1p8  43133  aks6d1c2lem3  43144  aks6d1c2lem4  43145  aks6d1c2  43148  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks6d1c6lem4  43191  aks6d1c6isolem1  43192  aks6d1c6isolem2  43193  aks6d1c6lem5  43195  aks5lem1  43204  aks5lem2  43205  aks5lem3a  43207  eliccre  46461  eliocre  46465  icoiccdif  46480  limccog  46576  lptioo1  46588  cncfiooicclem1  46847  ditgeqiooicc  46914  stoweidlem30  46984  stoweidlem31  46985  stoweidlem38  46992  stoweidlem44  46998  fourierdlem26  47087  fourierdlem32  47093  fourierdlem33  47094  fourierdlem37  47098  fourierdlem42  47103  fourierdlem54  47114  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  fourierdlem69  47129  fourierdlem79  47139  fourierdlem82  47142  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem111  47171  0sal  47274  hoidmv1lelem3  47547  smfdmss  47687  sigardiv  47815  sigarcol  47818  sharhght  47819  sigaradd  47820  cevathlem1  47821  cevathlem2  47822  cevath  47823  proththd  48643  perfectALTVlem2  48764  isuspgrim0  48936  gpgnbgrvtx0  49116  gpgnbgrvtx1  49117  itsclc0yqsol  49820  imaf1hom  50160  rr3fv1cld  50891