Theorem simp1d 1154

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp1bi  1157  f1dom3fv3dif  7248  f1dom3el3dif  7249  f1prex  7264  oeeui  8567  oeeu  8568  domssex2  9105  domssex  9106  cantnflem1a  9637  cantnflem1b  9638  cantnflem1c  9639  cantnflem1d  9640  cantnflem1  9641  cantnflem3  9643  cantnflem4  9644  fpwwe2lem6  10591  canthnumlem  10603  canthp1lem2  10608  wuntr  10660  lelttrdi  11342  supmul1  12158  supmullem1  12159  supmullem2  12160  supmul  12161  ixxdisj  13361  ixxun  13362  ixxss1  13364  ixxss2  13365  ixxss12  13366  ixxub  13367  ixxlb  13368  iccss2  13418  iocssre  13428  icossre  13429  iccssre  13430  icodisj  13477  iccf1o  13497  xov1plusxeqvd  13499  fzen  13543  intfracq  13866  fldiv  13867  remul  15139  01sqrexlem6  15257  resqrtth  15265  sqrtth  15375  ruclem6  16250  ruclem9  16253  ruclem12  16256  gcdn0cl  16519  crth  16796  phimullem  16797  eulerthlem1  16799  eulerthlem2  16800  pcpremul  16862  prmreclem3  16937  sectcan  17771  sectco  17772  sectmon  17798  monsect  17799  funcf1  17882  funcsect  17888  invfuc  17993  coapm  18087  catciso  18127  psrel  18584  pstr  18592  mhmf  18806  submss  18826  eqger  19202  eqgcpbl  19206  gaorber  19331  orbstafun  19334  cayleyth  19438  dprdgrp  20030  dprdff  20037  ablfac1a  20094  ablfac1b  20095  lmodvscl  20925  lbsss  21124  2idlcpblrng  21321  evlsval3  22122  mpfind  22148  mdetunilem2  22653  mdetunilem5  22656  mdetunilem6  22657  chfacfisfcpmat  22895  cnptop1  23282  lmfpm  23335  lmff  23341  lmcnp  23344  flimtop  24005  tlmtmd  24227  ustssxp  24245  ustdiag  24249  ustfilxp  24253  ustbas2  24265  tusbas  24307  imasdsf1olem  24413  xmeter  24473  tmsbas  24523  metustexhalf  24596  nlmngp  24717  qdensere  24809  blcvx  24838  tgqioo  24840  icccmplem2  24864  reconnlem1  24867  cnmpopc  24970  icoopnst  24981  iocopnst  24982  iccpnfcnv  24986  phtpcer  25037  phtpcco2  25041  pcohtpylem  25061  pcohtpy  25062  pcopt  25064  pcopt2  25065  pcorevlem  25068  pcorev2  25070  pcophtb  25071  om1addcl  25075  pi1grplem  25091  pi1inv  25094  pi1xfrf  25095  pi1xfr  25097  pi1xfrcnvlem  25098  pi1xfrcnv  25099  pi1cof  25101  pi1coghm  25103  cphphl  25213  cphreccllem  25220  cphsqrtcl2  25228  phclm  25274  tcphcph  25279  lmcau  25355  bcthlem4  25369  minveclem4c  25467  minveclem2  25468  minveclem3b  25470  minveclem4  25474  minveclem6  25476  ivthicc  25500  ovolfsval  25512  ovollb2lem  25530  ovolshftlem1  25551  ovolscalem1  25555  ovolicc2lem2  25560  ovolicc2lem5  25563  ovolicopnf  25566  ioombl1lem1  25600  ioombl1lem3  25602  ioombl1lem4  25603  uniioovol  25621  uniioombllem2a  25624  uniioombllem2  25625  uniioombllem3a  25626  uniioombllem3  25627  uniioombllem4  25628  uniioombllem6  25630  vitalilem2  25651  vitalilem3  25652  vitalilem4  25653  i1ff  25718  itg2monolem1  25792  itgreval  25839  ibladd  25863  iblabslem  25870  itgspliticc  25879  itgsplitioo  25880  ditgcl  25900  ditgswap  25901  ditgsplitlem  25902  ditgsplit  25903  limcresi  25927  dvlip2  26037  dveq0  26042  dvcnvre  26061  dvfsumlem2  26069  ftc1a  26079  ply1rem  26206  facth1  26207  fta1glem1  26208  fta1glem2  26209  ig1pcl  26219  ig1pdvds  26220  plyrem  26346  facth  26347  vieta1lem1  26351  vieta1lem2  26352  aaliou3lem3  26385  aaliou3lem7  26390  pserulm  26462  psercnlem2  26464  psercn  26466  pserdvlem1  26467  pserdvlem2  26468  pserdv  26469  abelth2  26482  coseq00topi  26544  coseq0negpitopi  26545  cosordlem  26572  efif1olem1  26584  dvloglem  26690  loglesqrt  26803  relogbval  26814  nnlogbexp  26823  logbrec  26824  quart1  26898  quartlem2  26900  quartlem3  26901  quartlem4  26902  quart  26903  asinsinlem  26933  atanlogsublem  26957  atans2  26973  dvatan  26977  rlimcnp2  27008  divsqrtsumlem  27021  ftalem5  27118  ftalem7  27120  basellem4  27125  basellem5  27126  perfectlem2  27271  dchrinv  27302  chpdifbndlem1  27594  pntibndlem2  27632  pntlema  27637  pntlemb  27638  pntlemg  27639  pntlemh  27640  pntlemn  27641  pntlemq  27642  pntlemr  27643  pntlemj  27644  pntlemf  27646  pntlemk  27647  pntlemo  27648  pntlemp  27651  pntleml  27652  abvcxp  27656  cutscl  27852  cutsun12  27860  ltsrec  27871  addsproplem6  28044  addsprop  28046  addscld  28050  negsproplem6  28103  negsprop  28105  mulsproplem11  28196  mulsproplem12  28197  axtgbtwnid  28612  cgr3simp1  28666  hlne1  28751  hltr  28756  btwnhl  28760  mirhl  28825  opphllem4  28896  hlpasch  28902  inagswap  28987  inagne1  28988  dfcgrg2  29009  wlkf  29761  wlk1ewlk  29786  2wlkdlem6  30077  2wlkond  30083  2trlond  30085  grpofo  30648  vcablo  30718  nvvc  30764  sspba  30876  sspg  30877  minvecolem2  31024  minvecolem4c  31028  minvecolem4  31029  minvecolem5  31030  minvecolem6  31031  eleigveccl  32108  tpssad  32687  xrofsup  32919  eliccelico  32929  elicoelioo  32930  cyc3evpm  33291  slmdvscl  33355  slmdvsass  33358  imaslmod  33500  prmidlidl  33591  mxidlidl  33612  0ringmon1p  33714  irngss  33945  algextdeglem1  33975  constrsqrtcl  34037  baselsiga  34373  insiga  34395  ldsysgenld  34418  sigapildsys  34420  ldgenpisyslem1  34421  measfrge0  34461  sibfmbl  34593  eulerpartlemt  34629  eulerpartlemmf  34633  probfinmeasbALTV  34687  tg5segofs  34934  pfxwlk  35438  revwlk  35439  subgrwlk  35446  subfacp1lem2a  35494  subfacp1lem2b  35495  subfacp1lem3  35496  subfacp1lem4  35497  subfacp1lem5  35498  sconnpht2  35552  sconnpi1  35553  cvxsconn  35557  cvmlift2lem3  35619  cvmlift2lem5  35621  cvmlift2lem6  35622  cvmlift2lem7  35623  cvmlift2lem12  35628  cvmliftphtlem  35631  cvmliftpht  35632  cvmlift3lem2  35634  cvmlift3lem4  35636  cvmlift3lem5  35637  cvmlift3lem6  35638  msrf  35856  elmsta  35862  mthmpps  35896  mclsppslem  35897  mclspps  35898  weiunfrlem  36788  weiunpo  36789  weiunso  36790  weiunfr  36791  weiunse  36792  iblabsnclem  38146  dvasin  38167  isbnd3  38247  heiborlem3  38276  iccbnd  38303  rngohomf  38429  idlss  38479  lshplss  39569  opoccl  39782  opococ  39783  oplecon3  39787  hloml  39945  lclkrslem1  42125  lclkrslem2  42126  dvrelog2  42645  dvrelog3  42646  aks4d1p1p5  42656  primrootsunit1  42678  primrootscoprmpow  42680  primrootscoprbij  42683  primrootspoweq0  42687  aks6d1c1p2  42690  aks6d1c1p3  42691  aks6d1c1p4  42692  aks6d1c1p5  42693  aks6d1c1p7  42694  aks6d1c1p6  42695  aks6d1c1p8  42696  aks6d1c2lem3  42707  aks6d1c2lem4  42708  aks6d1c2  42711  aks6d1c6lem2  42752  aks6d1c6lem3  42753  aks6d1c6lem4  42754  aks6d1c6isolem1  42755  aks6d1c6isolem2  42756  aks6d1c6lem5  42758  aks5lem1  42767  aks5lem2  42768  aks5lem3a  42770  flt4lem5f  43203  flt4lem7  43205  nna4b4nsq  43206  eliccre  46045  eliocre  46049  icoiccdif  46064  limccog  46160  lptioo1  46172  cncfiooicclem1  46431  ditgeqiooicc  46498  stoweidlem30  46568  stoweidlem31  46569  stoweidlem38  46576  stoweidlem44  46582  fourierdlem26  46671  fourierdlem32  46677  fourierdlem33  46678  fourierdlem37  46682  fourierdlem42  46687  fourierdlem54  46698  fourierdlem63  46707  fourierdlem64  46708  fourierdlem65  46709  fourierdlem69  46713  fourierdlem79  46723  fourierdlem82  46726  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem111  46755  0sal  46858  hoidmv1lelem3  47131  smfdmss  47271  sigardiv  47399  sigarcol  47402  sharhght  47403  sigaradd  47404  cevathlem1  47405  cevathlem2  47406  cevath  47407  nthrucw  47426  proththd  48187  perfectALTVlem2  48308  isuspgrim0  48480  gpgnbgrvtx0  48660  gpgnbgrvtx1  48661  itsclc0yqsol  49350  imaf1hom  49693