Theorem simp1d 1141

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 1135	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp1bi  1144  f1dom3fv3dif  7181  f1dom3el3dif  7182  f1prex  7196  oeeui  8483  oeeu  8484  domssex2  8981  domssex  8982  cantnflem1a  9521  cantnflem1b  9522  cantnflem1c  9523  cantnflem1d  9524  cantnflem1  9525  cantnflem3  9527  cantnflem4  9528  fpwwe2lem6  10472  canthnumlem  10484  canthp1lem2  10489  wuntr  10541  lelttrdi  11217  supmul1  12024  supmullem1  12025  supmullem2  12026  supmul  12027  ixxdisj  13174  ixxun  13175  ixxss1  13177  ixxss2  13178  ixxss12  13179  ixxub  13180  ixxlb  13181  iccss2  13230  iocssre  13239  icossre  13240  iccssre  13241  icodisj  13288  iccf1o  13308  xov1plusxeqvd  13310  fzen  13353  intfracq  13659  fldiv  13660  remul  14919  sqrlem6  15038  resqrtth  15046  sqrtth  15155  ruclem6  16023  ruclem9  16026  ruclem12  16029  gcdn0cl  16288  crth  16556  phimullem  16557  eulerthlem1  16559  eulerthlem2  16560  pcpremul  16621  prmreclem3  16696  sectcan  17544  sectco  17545  sectmon  17571  monsect  17572  funcf1  17658  funcsect  17664  invfuc  17769  coapm  17863  catciso  17903  psrel  18364  pstr  18372  mhmf  18512  submss  18525  eqger  18882  eqgcpbl  18886  gaorber  18990  orbstafun  18993  cayleyth  19099  dprdgrp  19683  dprdff  19690  ablfac1a  19747  ablfac1b  19748  lmodvscl  20223  lbsss  20422  2idlcpbl  20588  assalmod  21150  mpfind  21400  mdetunilem2  21845  mdetunilem5  21848  mdetunilem6  21849  chfacfisfcpmat  22087  cnptop1  22476  lmfpm  22529  lmff  22535  lmcnp  22538  flimtop  23199  tlmtmd  23421  ustssxp  23439  ustdiag  23443  ustfilxp  23447  ustbas2  23460  tusbas  23503  imasdsf1olem  23609  xmeter  23669  tmsbas  23722  metustexhalf  23795  nlmngp  23924  qdensere  24016  blcvx  24044  tgqioo  24046  icccmplem2  24069  reconnlem1  24072  cnmpopc  24174  icoopnst  24185  iocopnst  24186  iccpnfcnv  24190  phtpcer  24241  phtpcco2  24245  pcohtpylem  24265  pcohtpy  24266  pcopt  24268  pcopt2  24269  pcorevlem  24272  pcorev2  24274  pcophtb  24275  om1addcl  24279  pi1grplem  24295  pi1inv  24298  pi1xfrf  24299  pi1xfr  24301  pi1xfrcnvlem  24302  pi1xfrcnv  24303  pi1cof  24305  pi1coghm  24307  cphphl  24418  cphreccllem  24425  cphsqrtcl2  24433  phclm  24479  tcphcph  24484  lmcau  24560  bcthlem4  24574  minveclem4c  24672  minveclem2  24673  minveclem3b  24675  minveclem4  24679  minveclem6  24681  ivthicc  24705  ovolfsval  24717  ovollb2lem  24735  ovolshftlem1  24756  ovolscalem1  24760  ovolicc2lem2  24765  ovolicc2lem5  24768  ovolicopnf  24771  ioombl1lem1  24805  ioombl1lem3  24807  ioombl1lem4  24808  uniioovol  24826  uniioombllem2a  24829  uniioombllem2  24830  uniioombllem3a  24831  uniioombllem3  24832  uniioombllem4  24833  uniioombllem6  24835  vitalilem2  24856  vitalilem3  24857  vitalilem4  24858  i1ff  24923  itg2monolem1  24998  itgreval  25044  ibladd  25068  iblabslem  25075  itgspliticc  25084  itgsplitioo  25085  ditgcl  25105  ditgswap  25106  ditgsplitlem  25107  ditgsplit  25108  limcresi  25132  dvlip2  25242  dveq0  25247  dvcnvre  25266  dvfsumlem2  25274  ftc1a  25284  ply1rem  25411  facth1  25412  fta1glem1  25413  fta1glem2  25414  ig1pcl  25423  ig1pdvds  25424  plyrem  25548  facth  25549  vieta1lem1  25553  vieta1lem2  25554  aaliou3lem3  25587  aaliou3lem7  25592  pserulm  25664  psercnlem2  25666  psercn  25668  pserdvlem1  25669  pserdvlem2  25670  pserdv  25671  abelth2  25684  coseq00topi  25742  coseq0negpitopi  25743  cosordlem  25769  efif1olem1  25781  dvloglem  25886  loglesqrt  25994  relogbval  26005  nnlogbexp  26014  logbrec  26015  quart1  26089  quartlem2  26091  quartlem3  26092  quartlem4  26093  quart  26094  asinsinlem  26124  atanlogsublem  26148  atans2  26164  dvatan  26168  rlimcnp2  26199  divsqrtsumlem  26212  ftalem5  26309  ftalem7  26311  basellem4  26316  basellem5  26317  perfectlem2  26461  dchrinv  26492  chpdifbndlem1  26784  pntibndlem2  26822  pntlema  26827  pntlemb  26828  pntlemg  26829  pntlemh  26830  pntlemn  26831  pntlemq  26832  pntlemr  26833  pntlemj  26834  pntlemf  26836  pntlemk  26837  pntlemo  26838  pntlemp  26841  pntleml  26842  abvcxp  26846  axtgbtwnid  26963  cgr3simp1  27017  hlne1  27102  hltr  27107  btwnhl  27111  mirhl  27176  opphllem4  27247  hlpasch  27253  inagswap  27338  inagne1  27339  dfcgrg2  27360  wlkf  28117  wlk1ewlk  28143  2wlkdlem6  28432  2wlkond  28438  2trlond  28440  grpofo  28997  vcablo  29067  nvvc  29113  sspba  29225  sspg  29226  minvecolem2  29373  minvecolem4c  29377  minvecolem4  29378  minvecolem5  29379  minvecolem6  29380  eleigveccl  30457  xrofsup  31225  eliccelico  31233  elicoelioo  31234  cyc3evpm  31552  slmdvscl  31602  slmdvsass  31605  imaslmod  31691  prmidlidl  31758  mxidlidl  31774  baselsiga  32223  insiga  32245  ldsysgenld  32268  sigapildsys  32270  ldgenpisyslem1  32271  measfrge0  32311  sibfmbl  32442  eulerpartlemt  32478  eulerpartlemmf  32482  probfinmeasbALTV  32536  tg5segofs  32793  pfxwlk  33224  revwlk  33225  subgrwlk  33233  subfacp1lem2a  33281  subfacp1lem2b  33282  subfacp1lem3  33283  subfacp1lem4  33284  subfacp1lem5  33285  sconnpht2  33339  sconnpi1  33340  cvxsconn  33344  cvmlift2lem3  33406  cvmlift2lem5  33408  cvmlift2lem6  33409  cvmlift2lem7  33410  cvmlift2lem12  33415  cvmliftphtlem  33418  cvmliftpht  33419  cvmlift3lem2  33421  cvmlift3lem4  33423  cvmlift3lem5  33424  cvmlift3lem6  33425  msrf  33643  elmsta  33649  mthmpps  33683  mclsppslem  33684  mclspps  33685  scutcl  34070  scutun12  34078  sltrec  34088  iblabsnclem  35912  dvasin  35933  isbnd3  36014  heiborlem3  36043  iccbnd  36070  rngohomf  36196  idlss  36246  lshplss  37215  opoccl  37428  opococ  37429  oplecon3  37433  hloml  37591  lclkrslem1  39772  lclkrslem2  39773  dvrelog2  40293  dvrelog3  40294  aks4d1p1p5  40304  metakunt8  40356  metakunt19  40367  metakunt21  40369  metakunt22  40370  metakunt25  40373  evlsval3  40488  flt4lem5f  40710  flt4lem7  40712  nna4b4nsq  40713  eliccre  43293  eliocre  43297  icoiccdif  43312  limccog  43411  lptioo1  43423  cncfiooicclem1  43684  ditgeqiooicc  43751  stoweidlem30  43821  stoweidlem31  43822  stoweidlem38  43829  stoweidlem44  43835  fourierdlem26  43924  fourierdlem32  43930  fourierdlem33  43931  fourierdlem37  43935  fourierdlem42  43940  fourierdlem54  43951  fourierdlem63  43960  fourierdlem64  43961  fourierdlem65  43962  fourierdlem69  43966  fourierdlem79  43976  fourierdlem82  43979  fourierdlem89  43986  fourierdlem90  43987  fourierdlem91  43988  fourierdlem111  44008  0sal  44111  hoidmv1lelem3  44382  smfdmss  44522  sigardiv  44642  sigarcol  44645  sharhght  44646  sigaradd  44647  cevathlem1  44648  cevathlem2  44649  cevath  44650  proththd  45331  perfectALTVlem2  45439  itsclc0yqsol  46375