Theorem simp1d 1160

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 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simp1bi  1163  f1dom3fv3dif  7268  f1dom3el3dif  7269  f1prex  7284  oeeui  8589  oeeu  8590  domssex2  9126  domssex  9127  cantnflem1a  9655  cantnflem1b  9656  cantnflem1c  9657  cantnflem1d  9658  cantnflem1  9659  cantnflem3  9661  cantnflem4  9662  fpwwe2lem6  10622  canthnumlem  10634  canthp1lem2  10639  wuntr  10691  lelttrdi  11373  supmul1  12185  supmullem1  12186  supmullem2  12187  supmul  12188  ixxdisj  13388  ixxun  13389  ixxss1  13391  ixxss2  13392  ixxss12  13393  ixxub  13394  ixxlb  13395  iccss2  13445  iocssre  13455  icossre  13456  iccssre  13457  icodisj  13504  iccf1o  13524  xov1plusxeqvd  13526  fzen  13570  intfracq  13894  fldiv  13895  remul  15182  01sqrexlem6  15300  resqrtth  15308  sqrtth  15418  ruclem6  16292  ruclem9  16295  ruclem12  16298  gcdn0cl  16561  crth  16838  phimullem  16839  eulerthlem1  16841  eulerthlem2  16842  pcpremul  16904  prmreclem3  16979  sectcan  17813  sectco  17814  sectmon  17840  monsect  17841  funcf1  17924  funcsect  17930  invfuc  18035  coapm  18129  catciso  18169  psrel  18626  pstr  18634  mhmf  18848  submss  18868  eqger  19247  eqgcpbl  19251  gaorber  19379  orbstafun  19382  cayleyth  19486  dprdgrp  20078  dprdff  20085  ablfac1a  20142  ablfac1b  20143  lmodvscl  20980  lbsss  21179  2idlcpblrng  21391  prmidlidl  21450  evlsval3  22221  mpfind  22247  mdetunilem2  22751  mdetunilem5  22754  mdetunilem6  22755  chfacfisfcpmat  22993  cnptop1  23380  lmfpm  23433  lmff  23439  lmcnp  23442  flimtop  24103  tlmtmd  24325  ustssxp  24343  ustdiag  24347  ustfilxp  24351  ustbas2  24363  tusbas  24405  imasdsf1olem  24511  xmeter  24571  tmsbas  24621  metustexhalf  24694  nlmngp  24815  qdensere  24907  blcvx  24936  tgqioo  24938  icccmplem2  24962  reconnlem1  24965  cnmpopc  25068  icoopnst  25079  iocopnst  25080  iccpnfcnv  25084  phtpcer  25135  phtpcco2  25139  pcohtpylem  25159  pcohtpy  25160  pcopt  25162  pcopt2  25163  pcorevlem  25166  pcorev2  25168  pcophtb  25169  om1addcl  25173  pi1grplem  25189  pi1inv  25192  pi1xfrf  25193  pi1xfr  25195  pi1xfrcnvlem  25196  pi1xfrcnv  25197  pi1cof  25199  pi1coghm  25201  cphphl  25311  cphreccllem  25318  cphsqrtcl2  25326  phclm  25372  tcphcph  25377  lmcau  25453  bcthlem4  25467  minveclem4c  25565  minveclem2  25566  minveclem3b  25568  minveclem4  25572  minveclem6  25574  ivthicc  25598  ovolfsval  25610  ovollb2lem  25628  ovolshftlem1  25649  ovolscalem1  25653  ovolicc2lem2  25658  ovolicc2lem5  25661  ovolicopnf  25664  ioombl1lem1  25698  ioombl1lem3  25700  ioombl1lem4  25701  uniioovol  25719  uniioombllem2a  25722  uniioombllem2  25723  uniioombllem3a  25724  uniioombllem3  25725  uniioombllem4  25726  uniioombllem6  25728  vitalilem2  25749  vitalilem3  25750  vitalilem4  25751  i1ff  25816  itg2monolem1  25890  itgreval  25937  ibladd  25961  iblabslem  25968  itgspliticc  25977  itgsplitioo  25978  ditgcl  25998  ditgswap  25999  ditgsplitlem  26000  ditgsplit  26001  limcresi  26025  dvlip2  26135  dveq0  26140  dvcnvre  26159  dvfsumlem2  26167  ftc1a  26177  ply1rem  26304  facth1  26305  fta1glem1  26306  fta1glem2  26307  ig1pcl  26317  ig1pdvds  26318  plyrem  26447  facth  26448  vieta1lem1  26452  vieta1lem2  26453  aaliou3lem3  26488  aaliou3lem7  26493  pserulm  26566  psercnlem2  26568  psercn  26570  pserdvlem1  26571  pserdvlem2  26572  pserdv  26573  abelth2  26586  coseq00topi  26648  coseq0negpitopi  26649  cosordlem  26676  efif1olem1  26688  dvloglem  26794  loglesqrt  26907  relogbval  26918  nnlogbexp  26927  logbrec  26928  quart1  27002  quartlem2  27004  quartlem3  27005  quartlem4  27006  quart  27007  asinsinlem  27037  atanlogsublem  27061  atans2  27077  dvatan  27081  rlimcnp2  27112  divsqrtsumlem  27125  ftalem5  27222  ftalem7  27224  basellem4  27229  basellem5  27230  perfectlem2  27375  dchrinv  27406  chpdifbndlem1  27698  pntibndlem2  27736  pntlema  27741  pntlemb  27742  pntlemg  27743  pntlemh  27744  pntlemn  27745  pntlemq  27746  pntlemr  27747  pntlemj  27748  pntlemf  27750  pntlemk  27751  pntlemo  27752  pntlemp  27755  pntleml  27756  abvcxp  27760  cutscl  27956  cutsun12  27964  ltsrec  27975  addsproplem6  28148  addsprop  28150  addscld  28154  negsproplem6  28207  negsprop  28209  mulsproplem11  28300  mulsproplem12  28301  axtgbtwnid  28716  cgr3simp1  28770  hlne1  28858  hltr  28863  btwnhl  28867  mirhl  28937  opphllem4  29012  hlpasch  29019  inagswap  29139  inagne1  29140  dfcgrg2  29161  wlkf  29945  wlk1ewlk  29970  2wlkdlem6  30261  2wlkond  30267  2trlond  30269  grpofo  30832  vcablo  30902  nvvc  30948  sspba  31060  sspg  31061  minvecolem2  31208  minvecolem4c  31212  minvecolem4  31213  minvecolem5  31214  minvecolem6  31215  eleigveccl  32292  tpssad  32866  xrofsup  33093  eliccelico  33103  elicoelioo  33104  cyc3evpm  33451  slmdvscl  33515  slmdvsass  33518  imaslmod  33654  mxidlidl  33727  0ringmon1p  33828  irngss  34058  algextdeglem1  34088  constrsqrtcl  34150  baselsiga  34486  insiga  34508  ldsysgenld  34531  sigapildsys  34533  ldgenpisyslem1  34534  measfrge0  34574  sibfmbl  34706  eulerpartlemt  34742  eulerpartlemmf  34746  probfinmeasbALTV  34800  tg5segofs  35044  pfxwlk  35597  revwlk  35598  subgrwlk  35605  subfacp1lem2a  35653  subfacp1lem2b  35654  subfacp1lem3  35655  subfacp1lem4  35656  subfacp1lem5  35657  sconnpht2  35711  sconnpi1  35712  cvxsconn  35716  cvmlift2lem3  35778  cvmlift2lem5  35780  cvmlift2lem6  35781  cvmlift2lem7  35782  cvmlift2lem12  35787  cvmliftphtlem  35790  cvmliftpht  35791  cvmlift3lem2  35793  cvmlift3lem4  35795  cvmlift3lem5  35796  cvmlift3lem6  35797  msrf  36015  elmsta  36021  mthmpps  36055  mclsppslem  36056  mclspps  36057  weiunfrlem  36956  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960  iblabsnclem  38315  dvasin  38336  isbnd3  38416  heiborlem3  38445  iccbnd  38472  rngohomf  38598  idlss  38648  lshplss  39736  opoccl  39949  opococ  39950  oplecon3  39954  hloml  40112  lclkrslem1  42292  lclkrslem2  42293  dvrelog2  42812  dvrelog3  42813  aks4d1p1p5  42823  primrootsunit1  42845  primrootscoprmpow  42847  primrootscoprbij  42850  primrootspoweq0  42854  aks6d1c1p2  42857  aks6d1c1p3  42858  aks6d1c1p4  42859  aks6d1c1p5  42860  aks6d1c1p7  42861  aks6d1c1p6  42862  aks6d1c1p8  42863  aks6d1c2lem3  42874  aks6d1c2lem4  42875  aks6d1c2  42878  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks6d1c6lem4  42921  aks6d1c6isolem1  42922  aks6d1c6isolem2  42923  aks6d1c6lem5  42925  aks5lem1  42934  aks5lem2  42935  aks5lem3a  42937  flt4lem5f  43372  flt4lem7  43374  nna4b4nsq  43375  eliccre  46204  eliocre  46208  icoiccdif  46223  limccog  46319  lptioo1  46331  cncfiooicclem1  46590  ditgeqiooicc  46657  stoweidlem30  46727  stoweidlem31  46728  stoweidlem38  46735  stoweidlem44  46741  fourierdlem26  46830  fourierdlem32  46836  fourierdlem33  46837  fourierdlem37  46841  fourierdlem42  46846  fourierdlem54  46857  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  fourierdlem69  46872  fourierdlem79  46882  fourierdlem82  46885  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem111  46914  0sal  47017  hoidmv1lelem3  47290  smfdmss  47430  sigardiv  47558  sigarcol  47561  sharhght  47562  sigaradd  47563  cevathlem1  47564  cevathlem2  47565  cevath  47566  proththd  48349  perfectALTVlem2  48470  isuspgrim0  48642  gpgnbgrvtx0  48822  gpgnbgrvtx1  48823  itsclc0yqsol  49527  imaf1hom  49869