Theorem simp1d 1142

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 1136	. 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp1bi  1145  f1dom3fv3dif  7269  f1dom3el3dif  7270  f1prex  7284  oeeui  8604  oeeu  8605  domssex2  9139  domssex  9140  cantnflem1a  9682  cantnflem1b  9683  cantnflem1c  9684  cantnflem1d  9685  cantnflem1  9686  cantnflem3  9688  cantnflem4  9689  fpwwe2lem6  10633  canthnumlem  10645  canthp1lem2  10650  wuntr  10702  lelttrdi  11380  supmul1  12187  supmullem1  12188  supmullem2  12189  supmul  12190  ixxdisj  13343  ixxun  13344  ixxss1  13346  ixxss2  13347  ixxss12  13348  ixxub  13349  ixxlb  13350  iccss2  13399  iocssre  13408  icossre  13409  iccssre  13410  icodisj  13457  iccf1o  13477  xov1plusxeqvd  13479  fzen  13522  intfracq  13828  fldiv  13829  remul  15080  01sqrexlem6  15198  resqrtth  15206  sqrtth  15315  ruclem6  16182  ruclem9  16185  ruclem12  16188  gcdn0cl  16447  crth  16715  phimullem  16716  eulerthlem1  16718  eulerthlem2  16719  pcpremul  16780  prmreclem3  16855  sectcan  17706  sectco  17707  sectmon  17733  monsect  17734  funcf1  17820  funcsect  17826  invfuc  17931  coapm  18025  catciso  18065  psrel  18526  pstr  18534  mhmf  18711  submss  18726  eqger  19094  eqgcpbl  19098  gaorber  19213  orbstafun  19216  cayleyth  19324  dprdgrp  19916  dprdff  19923  ablfac1a  19980  ablfac1b  19981  lmodvscl  20632  lbsss  20832  2idlcpblrng  21020  mpfind  21889  mdetunilem2  22335  mdetunilem5  22338  mdetunilem6  22339  chfacfisfcpmat  22577  cnptop1  22966  lmfpm  23019  lmff  23025  lmcnp  23028  flimtop  23689  tlmtmd  23911  ustssxp  23929  ustdiag  23933  ustfilxp  23937  ustbas2  23950  tusbas  23993  imasdsf1olem  24099  xmeter  24159  tmsbas  24212  metustexhalf  24285  nlmngp  24414  qdensere  24506  blcvx  24534  tgqioo  24536  icccmplem2  24559  reconnlem1  24562  cnmpopc  24668  icoopnst  24679  iocopnst  24680  iccpnfcnv  24684  phtpcer  24735  phtpcco2  24739  pcohtpylem  24759  pcohtpy  24760  pcopt  24762  pcopt2  24763  pcorevlem  24766  pcorev2  24768  pcophtb  24769  om1addcl  24773  pi1grplem  24789  pi1inv  24792  pi1xfrf  24793  pi1xfr  24795  pi1xfrcnvlem  24796  pi1xfrcnv  24797  pi1cof  24799  pi1coghm  24801  cphphl  24912  cphreccllem  24919  cphsqrtcl2  24927  phclm  24973  tcphcph  24978  lmcau  25054  bcthlem4  25068  minveclem4c  25166  minveclem2  25167  minveclem3b  25169  minveclem4  25173  minveclem6  25175  ivthicc  25199  ovolfsval  25211  ovollb2lem  25229  ovolshftlem1  25250  ovolscalem1  25254  ovolicc2lem2  25259  ovolicc2lem5  25262  ovolicopnf  25265  ioombl1lem1  25299  ioombl1lem3  25301  ioombl1lem4  25302  uniioovol  25320  uniioombllem2a  25323  uniioombllem2  25324  uniioombllem3a  25325  uniioombllem3  25326  uniioombllem4  25327  uniioombllem6  25329  vitalilem2  25350  vitalilem3  25351  vitalilem4  25352  i1ff  25417  itg2monolem1  25492  itgreval  25538  ibladd  25562  iblabslem  25569  itgspliticc  25578  itgsplitioo  25579  ditgcl  25599  ditgswap  25600  ditgsplitlem  25601  ditgsplit  25602  limcresi  25626  dvlip2  25736  dveq0  25741  dvcnvre  25760  dvfsumlem2  25768  ftc1a  25778  ply1rem  25905  facth1  25906  fta1glem1  25907  fta1glem2  25908  ig1pcl  25917  ig1pdvds  25918  plyrem  26042  facth  26043  vieta1lem1  26047  vieta1lem2  26048  aaliou3lem3  26081  aaliou3lem7  26086  pserulm  26158  psercnlem2  26160  psercn  26162  pserdvlem1  26163  pserdvlem2  26164  pserdv  26165  abelth2  26178  coseq00topi  26236  coseq0negpitopi  26237  cosordlem  26263  efif1olem1  26275  dvloglem  26380  loglesqrt  26490  relogbval  26501  nnlogbexp  26510  logbrec  26511  quart1  26585  quartlem2  26587  quartlem3  26588  quartlem4  26589  quart  26590  asinsinlem  26620  atanlogsublem  26644  atans2  26660  dvatan  26664  rlimcnp2  26695  divsqrtsumlem  26708  ftalem5  26805  ftalem7  26807  basellem4  26812  basellem5  26813  perfectlem2  26957  dchrinv  26988  chpdifbndlem1  27280  pntibndlem2  27318  pntlema  27323  pntlemb  27324  pntlemg  27325  pntlemh  27326  pntlemn  27327  pntlemq  27328  pntlemr  27329  pntlemj  27330  pntlemf  27332  pntlemk  27333  pntlemo  27334  pntlemp  27337  pntleml  27338  abvcxp  27342  scutcl  27528  scutun12  27536  sltrec  27546  addsproplem6  27684  addsprop  27686  addscld  27690  negsproplem6  27734  negsprop  27736  mulsproplem11  27809  mulsproplem12  27810  axtgbtwnid  27972  cgr3simp1  28026  hlne1  28111  hltr  28116  btwnhl  28120  mirhl  28185  opphllem4  28256  hlpasch  28262  inagswap  28347  inagne1  28348  dfcgrg2  28369  wlkf  29126  wlk1ewlk  29152  2wlkdlem6  29440  2wlkond  29446  2trlond  29448  grpofo  30007  vcablo  30077  nvvc  30123  sspba  30235  sspg  30236  minvecolem2  30383  minvecolem4c  30387  minvecolem4  30388  minvecolem5  30389  minvecolem6  30390  eleigveccl  31467  xrofsup  32235  eliccelico  32243  elicoelioo  32244  cyc3evpm  32567  slmdvscl  32617  slmdvsass  32620  imaslmod  32726  prmidlidl  32824  mxidlidl  32841  0ringmon1p  32898  irngss  33028  algextdeglem1  33050  baselsiga  33399  insiga  33421  ldsysgenld  33444  sigapildsys  33446  ldgenpisyslem1  33447  measfrge0  33487  sibfmbl  33620  eulerpartlemt  33656  eulerpartlemmf  33660  probfinmeasbALTV  33714  tg5segofs  33971  pfxwlk  34400  revwlk  34401  subgrwlk  34409  subfacp1lem2a  34457  subfacp1lem2b  34458  subfacp1lem3  34459  subfacp1lem4  34460  subfacp1lem5  34461  sconnpht2  34515  sconnpi1  34516  cvxsconn  34520  cvmlift2lem3  34582  cvmlift2lem5  34584  cvmlift2lem6  34585  cvmlift2lem7  34586  cvmlift2lem12  34591  cvmliftphtlem  34594  cvmliftpht  34595  cvmlift3lem2  34597  cvmlift3lem4  34599  cvmlift3lem5  34600  cvmlift3lem6  34601  msrf  34819  elmsta  34825  mthmpps  34859  mclsppslem  34860  mclspps  34861  gg-dvfsumlem2  35469  iblabsnclem  36854  dvasin  36875  isbnd3  36955  heiborlem3  36984  iccbnd  37011  rngohomf  37137  idlss  37187  lshplss  38154  opoccl  38367  opococ  38368  oplecon3  38372  hloml  38530  lclkrslem1  40711  lclkrslem2  40712  dvrelog2  41235  dvrelog3  41236  aks4d1p1p5  41246  metakunt8  41298  metakunt19  41309  metakunt21  41311  metakunt22  41312  metakunt25  41315  evlsval3  41433  flt4lem5f  41701  flt4lem7  41703  nna4b4nsq  41704  eliccre  44517  eliocre  44521  icoiccdif  44536  limccog  44635  lptioo1  44647  cncfiooicclem1  44908  ditgeqiooicc  44975  stoweidlem30  45045  stoweidlem31  45046  stoweidlem38  45053  stoweidlem44  45059  fourierdlem26  45148  fourierdlem32  45154  fourierdlem33  45155  fourierdlem37  45159  fourierdlem42  45164  fourierdlem54  45175  fourierdlem63  45184  fourierdlem64  45185  fourierdlem65  45186  fourierdlem69  45190  fourierdlem79  45200  fourierdlem82  45203  fourierdlem89  45210  fourierdlem90  45211  fourierdlem91  45212  fourierdlem111  45232  0sal  45335  hoidmv1lelem3  45608  smfdmss  45748  sigardiv  45876  sigarcol  45879  sharhght  45880  sigaradd  45881  cevathlem1  45882  cevathlem2  45883  cevath  45884  proththd  46581  perfectALTVlem2  46689  itsclc0yqsol  47538