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  7266  f1dom3el3dif  7267  f1prex  7281  oeeui  8601  oeeu  8602  domssex2  9136  domssex  9137  cantnflem1a  9679  cantnflem1b  9680  cantnflem1c  9681  cantnflem1d  9682  cantnflem1  9683  cantnflem3  9685  cantnflem4  9686  fpwwe2lem6  10630  canthnumlem  10642  canthp1lem2  10647  wuntr  10699  lelttrdi  11375  supmul1  12182  supmullem1  12183  supmullem2  12184  supmul  12185  ixxdisj  13338  ixxun  13339  ixxss1  13341  ixxss2  13342  ixxss12  13343  ixxub  13344  ixxlb  13345  iccss2  13394  iocssre  13403  icossre  13404  iccssre  13405  icodisj  13452  iccf1o  13472  xov1plusxeqvd  13474  fzen  13517  intfracq  13823  fldiv  13824  remul  15075  01sqrexlem6  15193  resqrtth  15201  sqrtth  15310  ruclem6  16177  ruclem9  16180  ruclem12  16183  gcdn0cl  16442  crth  16710  phimullem  16711  eulerthlem1  16713  eulerthlem2  16714  pcpremul  16775  prmreclem3  16850  sectcan  17701  sectco  17702  sectmon  17728  monsect  17729  funcf1  17815  funcsect  17821  invfuc  17926  coapm  18020  catciso  18060  psrel  18521  pstr  18529  mhmf  18676  submss  18689  eqger  19057  eqgcpbl  19061  gaorber  19171  orbstafun  19174  cayleyth  19282  dprdgrp  19874  dprdff  19881  ablfac1a  19938  ablfac1b  19939  lmodvscl  20488  lbsss  20687  2idlcpbl  20870  mpfind  21669  mdetunilem2  22114  mdetunilem5  22117  mdetunilem6  22118  chfacfisfcpmat  22356  cnptop1  22745  lmfpm  22798  lmff  22804  lmcnp  22807  flimtop  23468  tlmtmd  23690  ustssxp  23708  ustdiag  23712  ustfilxp  23716  ustbas2  23729  tusbas  23772  imasdsf1olem  23878  xmeter  23938  tmsbas  23991  metustexhalf  24064  nlmngp  24193  qdensere  24285  blcvx  24313  tgqioo  24315  icccmplem2  24338  reconnlem1  24341  cnmpopc  24443  icoopnst  24454  iocopnst  24455  iccpnfcnv  24459  phtpcer  24510  phtpcco2  24514  pcohtpylem  24534  pcohtpy  24535  pcopt  24537  pcopt2  24538  pcorevlem  24541  pcorev2  24543  pcophtb  24544  om1addcl  24548  pi1grplem  24564  pi1inv  24567  pi1xfrf  24568  pi1xfr  24570  pi1xfrcnvlem  24571  pi1xfrcnv  24572  pi1cof  24574  pi1coghm  24576  cphphl  24687  cphreccllem  24694  cphsqrtcl2  24702  phclm  24748  tcphcph  24753  lmcau  24829  bcthlem4  24843  minveclem4c  24941  minveclem2  24942  minveclem3b  24944  minveclem4  24948  minveclem6  24950  ivthicc  24974  ovolfsval  24986  ovollb2lem  25004  ovolshftlem1  25025  ovolscalem1  25029  ovolicc2lem2  25034  ovolicc2lem5  25037  ovolicopnf  25040  ioombl1lem1  25074  ioombl1lem3  25076  ioombl1lem4  25077  uniioovol  25095  uniioombllem2a  25098  uniioombllem2  25099  uniioombllem3a  25100  uniioombllem3  25101  uniioombllem4  25102  uniioombllem6  25104  vitalilem2  25125  vitalilem3  25126  vitalilem4  25127  i1ff  25192  itg2monolem1  25267  itgreval  25313  ibladd  25337  iblabslem  25344  itgspliticc  25353  itgsplitioo  25354  ditgcl  25374  ditgswap  25375  ditgsplitlem  25376  ditgsplit  25377  limcresi  25401  dvlip2  25511  dveq0  25516  dvcnvre  25535  dvfsumlem2  25543  ftc1a  25553  ply1rem  25680  facth1  25681  fta1glem1  25682  fta1glem2  25683  ig1pcl  25692  ig1pdvds  25693  plyrem  25817  facth  25818  vieta1lem1  25822  vieta1lem2  25823  aaliou3lem3  25856  aaliou3lem7  25861  pserulm  25933  psercnlem2  25935  psercn  25937  pserdvlem1  25938  pserdvlem2  25939  pserdv  25940  abelth2  25953  coseq00topi  26011  coseq0negpitopi  26012  cosordlem  26038  efif1olem1  26050  dvloglem  26155  loglesqrt  26263  relogbval  26274  nnlogbexp  26283  logbrec  26284  quart1  26358  quartlem2  26360  quartlem3  26361  quartlem4  26362  quart  26363  asinsinlem  26393  atanlogsublem  26417  atans2  26433  dvatan  26437  rlimcnp2  26468  divsqrtsumlem  26481  ftalem5  26578  ftalem7  26580  basellem4  26585  basellem5  26586  perfectlem2  26730  dchrinv  26761  chpdifbndlem1  27053  pntibndlem2  27091  pntlema  27096  pntlemb  27097  pntlemg  27098  pntlemh  27099  pntlemn  27100  pntlemq  27101  pntlemr  27102  pntlemj  27103  pntlemf  27105  pntlemk  27106  pntlemo  27107  pntlemp  27110  pntleml  27111  abvcxp  27115  scutcl  27300  scutun12  27308  sltrec  27318  addsproplem6  27455  addsprop  27457  addscld  27461  negsproplem6  27504  negsprop  27506  mulsproplem11  27579  mulsproplem12  27580  axtgbtwnid  27714  cgr3simp1  27768  hlne1  27853  hltr  27858  btwnhl  27862  mirhl  27927  opphllem4  27998  hlpasch  28004  inagswap  28089  inagne1  28090  dfcgrg2  28111  wlkf  28868  wlk1ewlk  28894  2wlkdlem6  29182  2wlkond  29188  2trlond  29190  grpofo  29747  vcablo  29817  nvvc  29863  sspba  29975  sspg  29976  minvecolem2  30123  minvecolem4c  30127  minvecolem4  30128  minvecolem5  30129  minvecolem6  30130  eleigveccl  31207  xrofsup  31975  eliccelico  31983  elicoelioo  31984  cyc3evpm  32304  slmdvscl  32354  slmdvsass  32357  imaslmod  32463  prmidlidl  32557  mxidlidl  32574  0ringmon1p  32631  irngss  32746  baselsiga  33108  insiga  33130  ldsysgenld  33153  sigapildsys  33155  ldgenpisyslem1  33156  measfrge0  33196  sibfmbl  33329  eulerpartlemt  33365  eulerpartlemmf  33369  probfinmeasbALTV  33423  tg5segofs  33680  pfxwlk  34109  revwlk  34110  subgrwlk  34118  subfacp1lem2a  34166  subfacp1lem2b  34167  subfacp1lem3  34168  subfacp1lem4  34169  subfacp1lem5  34170  sconnpht2  34224  sconnpi1  34225  cvxsconn  34229  cvmlift2lem3  34291  cvmlift2lem5  34293  cvmlift2lem6  34294  cvmlift2lem7  34295  cvmlift2lem12  34300  cvmliftphtlem  34303  cvmliftpht  34304  cvmlift3lem2  34306  cvmlift3lem4  34308  cvmlift3lem5  34309  cvmlift3lem6  34310  msrf  34528  elmsta  34534  mthmpps  34568  mclsppslem  34569  mclspps  34570  gg-dvfsumlem2  35178  iblabsnclem  36546  dvasin  36567  isbnd3  36647  heiborlem3  36676  iccbnd  36703  rngohomf  36829  idlss  36879  lshplss  37846  opoccl  38059  opococ  38060  oplecon3  38064  hloml  38222  lclkrslem1  40403  lclkrslem2  40404  dvrelog2  40924  dvrelog3  40925  aks4d1p1p5  40935  metakunt8  40987  metakunt19  40998  metakunt21  41000  metakunt22  41001  metakunt25  41004  evlsval3  41133  flt4lem5f  41400  flt4lem7  41402  nna4b4nsq  41403  eliccre  44208  eliocre  44212  icoiccdif  44227  limccog  44326  lptioo1  44338  cncfiooicclem1  44599  ditgeqiooicc  44666  stoweidlem30  44736  stoweidlem31  44737  stoweidlem38  44744  stoweidlem44  44750  fourierdlem26  44839  fourierdlem32  44845  fourierdlem33  44846  fourierdlem37  44850  fourierdlem42  44855  fourierdlem54  44866  fourierdlem63  44875  fourierdlem64  44876  fourierdlem65  44877  fourierdlem69  44881  fourierdlem79  44891  fourierdlem82  44894  fourierdlem89  44901  fourierdlem90  44902  fourierdlem91  44903  fourierdlem111  44923  0sal  45026  hoidmv1lelem3  45299  smfdmss  45439  sigardiv  45567  sigarcol  45570  sharhght  45571  sigaradd  45572  cevathlem1  45573  cevathlem2  45574  cevath  45575  proththd  46272  perfectALTVlem2  46380  2idlcpblrng  46756  itsclc0yqsol  47440