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 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:  simp1bi  1145  f1dom3fv3dif  7208  f1dom3el3dif  7209  f1prex  7224  oeeui  8523  oeeu  8524  domssex2  9057  domssex  9058  cantnflem1a  9582  cantnflem1b  9583  cantnflem1c  9584  cantnflem1d  9585  cantnflem1  9586  cantnflem3  9588  cantnflem4  9589  fpwwe2lem6  10534  canthnumlem  10546  canthp1lem2  10551  wuntr  10603  lelttrdi  11282  supmul1  12098  supmullem1  12099  supmullem2  12100  supmul  12101  ixxdisj  13262  ixxun  13263  ixxss1  13265  ixxss2  13266  ixxss12  13267  ixxub  13268  ixxlb  13269  iccss2  13319  iocssre  13329  icossre  13330  iccssre  13331  icodisj  13378  iccf1o  13398  xov1plusxeqvd  13400  fzen  13443  intfracq  13765  fldiv  13766  remul  15038  01sqrexlem6  15156  resqrtth  15164  sqrtth  15274  ruclem6  16146  ruclem9  16149  ruclem12  16152  gcdn0cl  16415  crth  16691  phimullem  16692  eulerthlem1  16694  eulerthlem2  16695  pcpremul  16757  prmreclem3  16832  sectcan  17664  sectco  17665  sectmon  17691  monsect  17692  funcf1  17775  funcsect  17781  invfuc  17886  coapm  17980  catciso  18020  psrel  18477  pstr  18485  mhmf  18699  submss  18719  eqger  19092  eqgcpbl  19096  gaorber  19222  orbstafun  19225  cayleyth  19329  dprdgrp  19921  dprdff  19928  ablfac1a  19985  ablfac1b  19986  lmodvscl  20813  lbsss  21013  2idlcpblrng  21210  mpfind  22043  mdetunilem2  22529  mdetunilem5  22532  mdetunilem6  22533  chfacfisfcpmat  22771  cnptop1  23158  lmfpm  23211  lmff  23217  lmcnp  23220  flimtop  23881  tlmtmd  24103  ustssxp  24121  ustdiag  24125  ustfilxp  24129  ustbas2  24141  tusbas  24183  imasdsf1olem  24289  xmeter  24349  tmsbas  24399  metustexhalf  24472  nlmngp  24593  qdensere  24685  blcvx  24714  tgqioo  24716  icccmplem2  24740  reconnlem1  24743  cnmpopc  24850  icoopnst  24864  iocopnst  24865  iccpnfcnv  24870  phtpcer  24922  phtpcco2  24927  pcohtpylem  24947  pcohtpy  24948  pcopt  24950  pcopt2  24951  pcorevlem  24954  pcorev2  24956  pcophtb  24957  om1addcl  24961  pi1grplem  24977  pi1inv  24980  pi1xfrf  24981  pi1xfr  24983  pi1xfrcnvlem  24984  pi1xfrcnv  24985  pi1cof  24987  pi1coghm  24989  cphphl  25099  cphreccllem  25106  cphsqrtcl2  25114  phclm  25160  tcphcph  25165  lmcau  25241  bcthlem4  25255  minveclem4c  25353  minveclem2  25354  minveclem3b  25356  minveclem4  25360  minveclem6  25362  ivthicc  25387  ovolfsval  25399  ovollb2lem  25417  ovolshftlem1  25438  ovolscalem1  25442  ovolicc2lem2  25447  ovolicc2lem5  25450  ovolicopnf  25453  ioombl1lem1  25487  ioombl1lem3  25489  ioombl1lem4  25490  uniioovol  25508  uniioombllem2a  25511  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem6  25517  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  i1ff  25605  itg2monolem1  25679  itgreval  25726  ibladd  25750  iblabslem  25757  itgspliticc  25766  itgsplitioo  25767  ditgcl  25787  ditgswap  25788  ditgsplitlem  25789  ditgsplit  25790  limcresi  25814  dvlip2  25928  dveq0  25933  dvcnvre  25952  dvfsumlem2  25961  dvfsumlem2OLD  25962  ftc1a  25972  ply1rem  26099  facth1  26100  fta1glem1  26101  fta1glem2  26102  ig1pcl  26112  ig1pdvds  26113  plyrem  26241  facth  26242  vieta1lem1  26246  vieta1lem2  26247  aaliou3lem3  26280  aaliou3lem7  26285  pserulm  26359  psercnlem2  26362  psercn  26364  pserdvlem1  26365  pserdvlem2  26366  pserdv  26367  abelth2  26380  coseq00topi  26439  coseq0negpitopi  26440  cosordlem  26467  efif1olem1  26479  dvloglem  26585  loglesqrt  26699  relogbval  26710  nnlogbexp  26719  logbrec  26720  quart1  26794  quartlem2  26796  quartlem3  26797  quartlem4  26798  quart  26799  asinsinlem  26829  atanlogsublem  26853  atans2  26869  dvatan  26873  rlimcnp2  26904  divsqrtsumlem  26918  ftalem5  27015  ftalem7  27017  basellem4  27022  basellem5  27023  perfectlem2  27169  dchrinv  27200  chpdifbndlem1  27492  pntibndlem2  27530  pntlema  27535  pntlemb  27536  pntlemg  27537  pntlemh  27538  pntlemn  27539  pntlemq  27540  pntlemr  27541  pntlemj  27542  pntlemf  27544  pntlemk  27545  pntlemo  27546  pntlemp  27549  pntleml  27550  abvcxp  27554  scutcl  27744  scutun12  27752  sltrec  27763  addsproplem6  27918  addsprop  27920  addscld  27924  negsproplem6  27976  negsprop  27978  mulsproplem11  28066  mulsproplem12  28067  axtgbtwnid  28445  cgr3simp1  28499  hlne1  28584  hltr  28589  btwnhl  28593  mirhl  28658  opphllem4  28729  hlpasch  28735  inagswap  28820  inagne1  28821  dfcgrg2  28842  wlkf  29595  wlk1ewlk  29620  2wlkdlem6  29911  2wlkond  29917  2trlond  29919  grpofo  30481  vcablo  30551  nvvc  30597  sspba  30709  sspg  30710  minvecolem2  30857  minvecolem4c  30861  minvecolem4  30862  minvecolem5  30863  minvecolem6  30864  eleigveccl  31941  tpssad  32521  xrofsup  32754  eliccelico  32764  elicoelioo  32765  cyc3evpm  33126  slmdvscl  33190  slmdvsass  33193  imaslmod  33325  prmidlidl  33416  mxidlidl  33435  0ringmon1p  33527  irngss  33721  algextdeglem1  33751  constrsqrtcl  33813  baselsiga  34149  insiga  34171  ldsysgenld  34194  sigapildsys  34196  ldgenpisyslem1  34197  measfrge0  34237  sibfmbl  34369  eulerpartlemt  34405  eulerpartlemmf  34409  probfinmeasbALTV  34463  tg5segofs  34707  pfxwlk  35189  revwlk  35190  subgrwlk  35197  subfacp1lem2a  35245  subfacp1lem2b  35246  subfacp1lem3  35247  subfacp1lem4  35248  subfacp1lem5  35249  sconnpht2  35303  sconnpi1  35304  cvxsconn  35308  cvmlift2lem3  35370  cvmlift2lem5  35372  cvmlift2lem6  35373  cvmlift2lem7  35374  cvmlift2lem12  35379  cvmliftphtlem  35382  cvmliftpht  35383  cvmlift3lem2  35385  cvmlift3lem4  35387  cvmlift3lem5  35388  cvmlift3lem6  35389  msrf  35607  elmsta  35613  mthmpps  35647  mclsppslem  35648  mclspps  35649  weiunfrlem  36529  weiunpo  36530  weiunso  36531  weiunfr  36532  weiunse  36533  iblabsnclem  37743  dvasin  37764  isbnd3  37844  heiborlem3  37873  iccbnd  37900  rngohomf  38026  idlss  38076  lshplss  39100  opoccl  39313  opococ  39314  oplecon3  39318  hloml  39476  lclkrslem1  41656  lclkrslem2  41657  dvrelog2  42177  dvrelog3  42178  aks4d1p1p5  42188  primrootsunit1  42210  primrootscoprmpow  42212  primrootscoprbij  42215  primrootspoweq0  42219  aks6d1c1p2  42222  aks6d1c1p3  42223  aks6d1c1p4  42224  aks6d1c1p5  42225  aks6d1c1p7  42226  aks6d1c1p6  42227  aks6d1c1p8  42228  aks6d1c2lem3  42239  aks6d1c2lem4  42240  aks6d1c2  42243  aks6d1c6lem2  42284  aks6d1c6lem3  42285  aks6d1c6lem4  42286  aks6d1c6isolem1  42287  aks6d1c6isolem2  42288  aks6d1c6lem5  42290  aks5lem1  42299  aks5lem2  42300  aks5lem3a  42302  evlsval3  42677  flt4lem5f  42775  flt4lem7  42777  nna4b4nsq  42778  eliccre  45629  eliocre  45633  icoiccdif  45648  limccog  45744  lptioo1  45756  cncfiooicclem1  46015  ditgeqiooicc  46082  stoweidlem30  46152  stoweidlem31  46153  stoweidlem38  46160  stoweidlem44  46166  fourierdlem26  46255  fourierdlem32  46261  fourierdlem33  46262  fourierdlem37  46266  fourierdlem42  46271  fourierdlem54  46282  fourierdlem63  46291  fourierdlem64  46292  fourierdlem65  46293  fourierdlem69  46297  fourierdlem79  46307  fourierdlem82  46310  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem111  46339  0sal  46442  hoidmv1lelem3  46715  smfdmss  46855  sigardiv  46983  sigarcol  46986  sharhght  46987  sigaradd  46988  cevathlem1  46989  cevathlem2  46990  cevath  46991  nthrucw  47008  proththd  47738  perfectALTVlem2  47846  isuspgrim0  48018  gpgnbgrvtx0  48198  gpgnbgrvtx1  48199  itsclc0yqsol  48889  imaf1hom  49233