Theorem simp2d 1166

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

Hypothesis

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

Assertion

Ref	Expression
simp2d	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2d

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simp2bi  1169  f1dom3fv3dif  6745  f1dom3el3dif  6746  f1prex  6759  oeeui  7915  resixp  8176  domssex  8356  cantnflem1a  8825  cantnflem1d  8828  cantnflem3  8831  cantnflem4  8832  fpwwe2lem7  9739  canthnumlem  9751  canthp1lem2  9756  wun0  9821  lelttrdi  10480  supmullem2  11275  supmul  11276  ixxdisj  12404  ixxun  12405  ixxss1  12407  ixxss2  12408  ixxss12  12409  ixxub  12410  ixxlb  12411  ubioo  12421  elicore  12440  iccgelb  12444  iccss2  12458  icodisj  12514  xov1plusxeqvd  12537  fldiv  12879  immul  14095  sqrtge0  14217  sqrtrege0  14324  icco1  14490  ruclem2  15177  ruclem3  15178  ruclem8  15182  ruclem12  15186  gcddvds  15440  crth  15696  phimullem  15697  eulerthlem1  15699  eulerthlem2  15700  prmreclem3  15835  sectcan  16615  sectco  16616  sectmon  16642  monsect  16643  funcixp  16727  funcsect  16732  invfuc  16834  coapm  16921  catciso  16957  posasymb  17153  ipodrsima  17366  pstr2  17406  psdmrn  17408  psref  17409  mhmlin  17543  subm0cl  17553  eqger  17842  eqgcpbl  17846  gaorber  17938  orbstafun  17941  cayleyth  18032  pmtrrn2  18077  pmtrfinv  18078  dfod2  18178  sylow2blem1  18232  dprdf  18603  dprdff  18609  dprdfcl  18610  dprdsplit  18645  dpjcntz  18649  ablfac1a  18666  ablfac1b  18667  lmodvsdi  19086  lbssp  19282  2idlcpbl  19439  assaring  19525  mpff  19737  mpfaddcl  19738  mpfmulcl  19739  mpfind  19740  pf1rcl  19917  mpfpf1  19919  mdetunilem2  20627  mdetunilem5  20630  mdetunilem6  20631  chfacfisfcpmat  20870  pnfnei  21235  cnptop2  21258  lmcl  21312  lmcnp  21319  flimfil  21983  tlmlmod  22202  ustbasel  22220  ustincl  22221  ustinvel  22223  ustfilxp  22226  tusunif  22283  imasdsf1olem  22388  xmeter  22448  tmsds  22499  metustexhalf  22571  nlmlmod  22692  qdensere  22783  blcvx  22811  tgqioo  22813  icccmplem2  22836  reconnlem1  22839  cnmpt2pc  22937  phtpcer  23004  phtpcco2  23008  pcohtpylem  23028  pcohtpy  23029  pcophtb  23038  om1addcl  23042  pi1blem  23048  pi1cpbl  23053  pi1grplem  23058  pi1inv  23061  pi1xfrf  23062  pi1xfr  23064  pi1xfrcnvlem  23065  pi1cof  23068  pi1coghm  23070  cphnlm  23181  cphsqrtcl2  23195  tchcph  23245  lmcau  23321  bcthlem4  23334  minveclem4c  23407  minveclem2  23408  minveclem3b  23410  minveclem4  23414  minveclem6  23416  ivthicc  23438  ovolfsval  23450  ovollb2lem  23468  ovolshftlem1  23489  ovolscalem1  23493  ovolicc1  23496  ovolicc2lem2  23498  ovolicc2lem4  23500  ovolicc2lem5  23501  ovolicopnf  23504  ioombl1lem1  23538  ioombl1lem3  23540  ioombl1lem4  23541  uniioovol  23559  uniioombllem2a  23562  uniioombllem2  23563  uniioombllem3a  23564  uniioombllem3  23565  uniioombllem4  23566  uniioombllem6  23568  dyadmaxlem  23577  volivth  23587  vitalilem2  23589  vitalilem5  23592  i1frn  23657  itg2monolem1  23730  itgcnlem  23769  itgrevallem1  23774  itgreval  23776  itgle  23789  ibladd  23800  iblabslem  23807  itgspliticc  23816  itgsplitioo  23817  ditgcl  23835  ditgswap  23836  ditgsplitlem  23837  limcdif  23853  limcresi  23862  limccnp  23868  limccnp2  23869  limcco  23870  dvlip  23969  dvlip2  23971  dveq0  23976  dvgt0lem1  23978  dvivthlem1  23984  dvcnvrelem1  23993  dvcnvre  23995  dvfsumlem2  24003  ftc1lem1  24011  ftc1a  24013  ftc1lem4  24015  ftc2ditglem  24021  itgsubstlem  24024  ply1rem  24136  fta1glem1  24138  ig1pdvds  24149  plyrem  24273  facth  24274  fta1lem  24275  vieta1lem1  24278  vieta1lem2  24279  aaliou3lem3  24312  aaliou3lem4  24314  aaliou3lem7  24317  taylfvallem1  24324  tayl0  24329  taylply2  24335  radcnvle  24387  psercnlem2  24391  psercnlem1  24392  psercn  24393  pserdvlem1  24394  pserdvlem2  24395  abelth2  24409  coseq00topi  24468  coseq0negpitopi  24469  cosordlem  24491  tanord1  24497  efif1olem1  24502  loglesqrt  24712  logreclem  24713  relogbval  24723  nnlogbexp  24732  chordthmlem4  24775  quart1  24796  quartlem2  24798  quartlem3  24799  quartlem4  24800  quart  24801  acosbnd  24840  atancj  24850  atanlogsublem  24855  atantan  24863  atanbndlem  24865  dvatan  24875  atantayl  24877  rlimcnp2  24906  divsqrtsumlem  24919  ftalem5  25016  ftalem7  25018  basellem4  25023  basellem5  25024  perfectlem2  25168  dchrinv  25199  chpdifbndlem1  25455  pntibndlem2  25493  pntlemc  25497  pntlema  25498  pntlemb  25499  pntlemg  25500  pntlemh  25501  pntlemq  25503  pntlemr  25504  pntlemj  25505  pntlemi  25506  pntlemf  25507  pntlemk  25508  pntlemo  25509  pntleme  25510  pntlem3  25511  pntleml  25513  abvcxp  25517  axtgpasch  25579  cgr3simp2  25629  legso  25707  hlne2  25714  hlln  25715  mirhl  25787  hlperpnel  25830  opphllem4  25855  inagswap  25943  subumgredg2  26392  upgrres1  26420  nb3grprlem1  26497  wlkp  26739  wspthsswwlkn  27057  2wlkdlem6  27070  clwwisshclwwsn  27158  erclwwlkeqlen  27161  erclwwlksym  27163  erclwwlktr  27164  clwwlkn  27170  clwwlknwrd  27181  clwwlknonex2e  27278  extwwlkfablem1OLD  27516  grpoass  27685  vcsm  27744  nvf  27842  ssps  27912  minvecolem2  28058  minvecolem4c  28062  minvecolem4  28063  minvecolem5  28064  minvecolem6  28065  eigvec1  29148  eliccelico  29865  elicoelioo  29866  slmdvsdi  30092  slmdvs1  30097  pmtrto1cl  30173  cnre2csqlem  30280  lmxrge0  30322  sigaclci  30519  difelsiga  30520  insiga  30524  ldsysgenld  30547  sigapildsyslem  30548  sigapildsys  30549  ldgenpisyslem1  30550  measvnul  30593  sibfrn  30723  eulerpartlemt  30757  eulerpartlemmf  30761  tg5segofs  31075  subfacp1lem2a  31483  subfacp1lem3  31485  subfacp1lem4  31486  subfacp1lem5  31487  sconnpht2  31541  sconnpi1  31542  resconn  31549  cvmsss  31570  cvmsn0  31571  cvmlift2lem3  31608  cvmlift2lem7  31612  cvmliftphtlem  31620  cvmliftpht  31621  cvmlift3lem5  31626  cvmlift3lem6  31627  msrf  31760  elmsta  31766  mclsax  31787  mthmpps  31800  mclspps  31802  scutun12  32236  slerec  32242  ivthALT  32649  poimirlem17  33737  poimirlem20  33740  ibladdnc  33777  iblabsnclem  33783  ftc1cnnclem  33793  ftc1anc  33803  ftc2nc  33804  heiborlem3  33921  iccbnd  33948  rngohom1  34076  idl0cl  34126  maxidlnr  34150  lshpne  34760  opococ  34973  opexmid  34985  hlclat  35136  lclkrslem2  37316  gneispacern2  38934  cvgdvgrat  39009  iccshift  40222  iccsuble  40223  icoiccdif  40228  mullimc  40325  limccog  40329  mullimcf  40332  lptioo2  40340  limcmptdm  40344  limcicciooub  40346  xlimmnfvlem1  40535  xlimpnfvlem1  40539  icccncfext  40577  cncfioobdlem  40586  ditgeqiooicc  40652  itgsubsticc  40668  iblcncfioo  40670  itgiccshift  40672  itgperiod  40673  itgsbtaddcnst  40674  stoweidlem11  40704  stoweidlem31  40724  stoweidlem36  40729  stoweidlem38  40731  stoweidlem44  40737  stoweidlem62  40755  dirkercncflem1  40796  dirkercncflem4  40799  fourierdlem26  40826  fourierdlem32  40832  fourierdlem33  40833  fourierdlem37  40837  fourierdlem42  40842  fourierdlem54  40853  fourierdlem63  40862  fourierdlem64  40863  fourierdlem65  40864  fourierdlem69  40868  fourierdlem74  40873  fourierdlem75  40874  fourierdlem79  40878  fourierdlem81  40880  fourierdlem82  40881  fourierdlem89  40888  fourierdlem90  40889  fourierdlem91  40890  fourierdlem93  40892  fourierdlem101  40900  fourierdlem111  40910  saldifcl  41015  unisalgen2  41048  hoidmv1lelem3  41286  smff  41420  smfpimltxr  41435  sigardiv  41529  sigarcol  41532  sharhght  41533  sigaradd  41534  cevathlem1  41535  cevathlem2  41536  cevath  41537  proththd  42103  perfectALTVlem2  42203