Theorem simp3d 1141

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1135	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp3bi  1144  f1dom3fv3dif  7004  f1dom3el3dif  7005  oeeui  8211  resixp  8480  domssex2  8661  cantnflem1c  9134  cantnflem1  9136  cantnflem3  9138  cantnflem4  9139  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wununi  10117  wunpw  10118  wunpr  10120  lelttrdi  10791  ixxdisj  12741  ixxun  12742  ixxss1  12744  ixxss2  12745  ixxss12  12746  ixxub  12747  ixxlb  12748  lbioo  12757  elicore  12777  iccsupr  12820  icodisj  12854  xov1plusxeqvd  12876  intfracq  13222  fldiv  13223  seqf1olem2  13406  cjmul  14493  icco1  14889  sumtp  15096  rpnnen2lem10  15568  ruclem2  15577  ruclem3  15578  ruclem9  15583  ruclem12  15586  dvdslegcd  15843  crth  16105  eulerthlem1  16108  eulerthlem2  16109  pcpremul  16170  prmreclem2  16243  prmreclem3  16244  4sqlem13  16283  sectcan  17017  sectco  17018  sectmon  17044  monsect  17045  funcid  17132  funcco  17133  funcsect  17134  invfuc  17236  fuciso  17237  coapm  17323  catciso  17359  postr  17555  ipodrsima  17767  psref2  17806  psasym  17812  mhm0  17956  submcl  17969  submmnd  17970  eqger  18322  eqgcpbl  18326  gaorber  18430  orbsta  18435  cayleyth  18535  pmtrrn2  18580  pmtrfinv  18581  pmtrfmvdn0  18582  dfod2  18683  sylow2blem1  18737  sylow2blem3  18739  dprdcntz  19123  dprddisj  19124  dprdffsupp  19129  dpjdisj  19168  ablfac1a  19184  ablfac1b  19185  lmodvsdir  19651  lmhmlin  19800  lbsind  19845  2idlcpbl  20000  assasca  20551  mpfind  20779  mdetunilem2  21218  mdetunilem5  21221  mdetunilem6  21222  mnfnei  21826  cnprcl  21850  lmcvg  21867  lmff  21906  lmcls  21907  lmcnp  21909  fbasssin  22441  flimfil  22574  tgpconncomp  22718  tlmtrg  22795  ustssel  22811  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ustfilxp  22818  tustopn  22877  tususp  22878  imasdsf1olem  22980  xmeter  23040  xmetresbl  23044  tmstopn  23092  metustexhalf  23163  nlmnrg  23285  qdensere  23375  blcvx  23403  tgqioo  23405  icccmplem1  23427  icccmplem2  23428  reconnlem1  23431  cnmpopc  23533  iccpnfcnv  23549  phtpcer  23600  phtpcco2  23604  pcohtpy  23625  pcorev2  23633  pcophtb  23634  om1addcl  23638  pi1blem  23644  pi1cpbl  23649  pi1grplem  23654  pi1inv  23657  pi1xfrf  23658  pi1xfr  23660  pi1xfrcnvlem  23661  pi1cof  23664  pi1coghm  23666  cphreccllem  23783  cphsca  23784  cphsubrg  23785  cphsqrtcl2  23791  phclm  23836  tcphcph  23841  lmmcvg  23865  cmetcaulem  23892  lmcau  23917  bcthlem3  23930  bcthlem4  23931  minveclem4c  24029  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem6  24038  ivthicc  24062  ovollb2lem  24092  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem2  24122  ovolicc2lem3  24123  ovolicc2lem4  24124  ovolicc2lem5  24125  ioombl1lem1  24162  dyadmaxlem  24201  volivth  24211  vitalilem2  24213  vitalilem4  24215  i1fima2  24283  itg2monolem1  24354  itgcnlem  24393  itgrevallem1  24398  itgreval  24400  itgle  24413  ibladd  24424  iblabslem  24431  itgspliticc  24440  itgsplitioo  24441  ditgcl  24461  ditgswap  24462  ditgsplitlem  24463  limcdif  24479  limcresi  24488  limcres  24489  limccnp  24494  limccnp2  24495  limcun  24498  dvlip  24596  dvlip2  24598  dveq0  24603  dvgt0lem1  24605  dvivthlem1  24611  dvcnvrelem1  24620  dvcnvre  24622  dvfsumlem2  24630  ftc1lem1  24638  ftc1lem2  24639  ftc1a  24640  ftc1lem4  24642  ftc2  24647  ftc2ditglem  24648  itgsubstlem  24651  ply1rem  24764  fta1glem2  24767  ig1pdvds  24777  plyrem  24901  fta1lem  24903  vieta1lem2  24907  aaliou3lem3  24940  pserulm  25017  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  abelth2  25037  coseq00topi  25095  coseq0negpitopi  25096  cosordlem  25122  tanord1  25129  efif1olem1  25134  dvloglem  25239  efopnlem1  25247  logreclem  25348  relogbval  25358  nnlogbexp  25367  logbrec  25368  chordthmlem4  25421  quart1  25442  quartlem2  25444  quartlem3  25445  quart  25447  acosbnd  25486  atancj  25496  atanlogsublem  25501  atantan  25509  atanbndlem  25511  atans2  25517  dvatan  25521  atantayl  25523  divsqrtsumlem  25565  ftalem5  25662  basellem5  25670  ppisval  25689  chtleppi  25794  chpchtsum  25803  chpub  25804  mersenne  25811  perfectlem2  25814  dchrinv  25845  rplogsumlem2  26069  chpdifbndlem1  26137  pntibndlem2  26175  pntlema  26180  pntlemb  26181  pntlemg  26182  pntlemh  26183  pntlemr  26186  pntlemj  26187  pntlemf  26189  pntlemk  26190  pntlemo  26191  pntlemp  26194  pntleml  26195  abvcxp  26199  ostth2lem2  26218  axtgcont1  26262  cgr3simp3  26316  legso  26393  hlln  26401  hltr  26404  btwnhl  26408  mirhl  26473  mirbtwnhl  26474  opphllem4  26544  opphl  26548  hlpasch  26550  cgracgr  26612  cgraswap  26614  cgrahl  26621  cgracol  26622  inagswap  26635  inagne3  26638  dfcgrg2  26657  umgrnloopv  26899  umgredgne  26938  usgrnloopvALT  26991  frusgrnn0  27361  cusgrm1rusgr  27372  upgrclwlkcompim  27570  2wlkdlem6  27717  2wlkond  27723  2trlond  27725  numclwwlk2lem1  28161  numclwlk2lem2f1o  28164  tncp  28261  grpolidinv  28284  nvs  28446  nvz  28452  nvtri  28453  sspn  28519  minvecolem2  28658  minvecolem4c  28662  minvecolem4  28663  minvecolem5  28664  minvecolem6  28665  adj1  29716  eliccelico  30526  elicoelioo  30527  prmdvdsbc  30558  pmtrto1cl  30791  cyc3evpm  30842  slmdvsdir  30894  slmd0vs  30902  prmidl  31023  prmidlc  31032  qsidomlem2  31037  mxidlmax  31045  locfinreflem  31193  cnre2csqlem  31263  sigaclci  31501  unelsiga  31503  insiga  31506  unelldsys  31527  ldsysgenld  31529  sigapildsys  31531  ldgenpisyslem1  31532  measvun  31578  cntmeas  31595  sibfima  31706  signstfveq0  31957  tg5segofs  32054  bnj1018g  32345  bnj1018  32346  pfxwlk  32483  revwlk  32484  spthcycl  32489  acycgrcycl  32507  subfacp1lem3  32542  subfacp1lem4  32543  subfacp1lem5  32544  sconnpht2  32598  sconnpi1  32599  txsconn  32601  resconn  32606  cvmcn  32622  cvmsuni  32629  cvmsdisj  32630  cvmshmeo  32631  cvmlift2lem8  32670  cvmlift2lem13  32675  cvmliftphtlem  32677  cvmliftpht  32678  cvmlift3lem6  32684  msrf  32902  elmsta  32908  mthmpps  32942  mclsppslem  32943  scutun12  33384  slerec  33390  ivthALT  33796  relowlssretop  34780  ibladdnc  35114  iblabsnclem  35120  ftc2nc  35139  dvasin  35141  isbndx  35220  isbnd3  35222  prdsbnd  35231  heiborlem3  35251  iccbnd  35278  rngohomadd  35407  rngohommul  35408  idladdcl  35457  idllmulcl  35458  idlrmulcl  35459  maxidlmax  35481  pridlc  35509  eqvreltr  36002  lshpnelb  36280  lshpcmp  36284  oplecon3  36495  opnoncon  36504  hlcvl  36655  dochshpncl  38680  lclkrslem1  38833  lclkrslem2  38834  fzne2d  39268  metakunt8  39357  metakunt20  39369  metakunt21  39370  metakunt22  39371  metakunt24  39373  metakunt25  39374  acongrep  39921  ntrneinex  40780  neicvgmex  40820  gneispace0nelrn  40843  cvgdvgrat  41017  binomcxplemdvbinom  41057  eliocre  42146  iccshift  42155  iccsuble  42156  icoiccdif  42161  mullimc  42258  limccog  42262  limciccioolb  42263  mullimcf  42265  limcperiod  42270  lptioo2  42273  lptioo1  42274  neglimc  42289  addlimc  42290  0ellimcdiv  42291  reclimc  42295  xlimmnfvlem1  42474  xlimpnfvlem1  42478  icccncfext  42529  cncfioobdlem  42538  ditgeqiooicc  42602  iblspltprt  42615  iblcncfioo  42620  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem11  42653  stoweidlem31  42673  stoweidlem36  42678  stoweidlem38  42680  stoweidlem62  42704  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem26  42775  fourierdlem32  42781  fourierdlem33  42782  fourierdlem37  42786  fourierdlem42  42791  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem93  42841  fourierdlem101  42849  fourierdlem107  42855  fourierdlem109  42857  fourierdlem111  42859  salunicl  42958  saluncl  42959  hoidmv1lelem1  43230  hoidmv1lelem3  43232  hoidmvlelem1  43234  ovolval3  43286  iinhoiicclem  43312  smfpreimalt  43365  smfpreimaltf  43370  smfpreimale  43388  issmfgt  43390  smfpreimagt  43395  smfpreimage  43415  sigardiv  43475  sigarcol  43478  sharhght  43479  sigaradd  43480  cevathlem1  43481  cevathlem2  43482  cevath  43483  proththd  44132  perfectALTVlem2  44240