Theorem simp2bi 1146

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2bi	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1143	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  0ellim  6375  smodm  8277  erdm  8638  ixpfn  8833  winafp  10595  inar1  10673  inatsk  10676  tskuni  10681  grur1  10718  supmullem1  12099  supmullem2  12100  supmul  12101  eluzelz  12748  elfz3nn0  13523  elfzo0l  13658  ico01fl0  13725  addmodlteq  13855  cshco  14745  swrds2  14849  ef01bndlem  16095  sin01bnd  16096  cos01bnd  16097  sin01gt0  16101  bitsss  16339  smueqlem  16403  gznegcl  16849  gzcjcl  16850  gzaddcl  16851  gzmulcl  16852  gzabssqcl  16855  4sqlem4a  16865  cshwshashlem2  17010  structn0fun  17064  xpsff1o  17473  mre1cl  17498  drsbn0  18212  subgss  19042  symgfixelsi  19349  psgnunilem5  19408  pgpgrp  19508  slwsubg  19524  efgs1b  19650  efgsp1  19651  efgsres  19652  efgredeu  19666  efgred2  19667  efgcpbllemb  19669  omndtos  20041  rngmgp  20076  srgmgp  20111  ringmgp  20159  irrednu  20345  sdrgsubrg  20708  fldsdrgfld  20715  sdrgint  20721  primefld  20722  primefld0cl  20723  primefld1cl  20724  orngogrp  20780  lmodring  20803  lmodprop2d  20859  lssn0  20875  phlsrng  21570  ocvss  21609  obsss  21663  locfinbas  23438  fclsfil  23926  tmdtps  23992  tgptmd  23995  trgring  24087  tdrgdrng  24090  ngpms  24516  icopnfcnv  24868  xrhmeo  24872  oprpiece1res2  24878  phtpcer  24922  pcoval2  24944  pcoass  24952  clmsca  24993  cphsqrtcl  25112  bncms  25272  itg2ge0  25664  uc1pn0  26079  mon1pn0  26080  sinq12ge0  26445  cosq14gt0  26447  cosq14ge0  26448  cos02pilt1  26463  cosq34lt1  26464  sinord  26471  recosf1o  26472  resinf1o  26473  logrnaddcl  26511  logbcl  26705  relogbreexp  26713  atanf  26818  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  dvatan  26873  areambl  26896  rlimcnp  26903  emgt0  26945  harmoniclbnd  26947  harmonicbnd4  26949  lgamgulmlem2  26968  gausslemma2dlem1a  27304  2sqlem2  27357  2sqlem3  27359  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  logdivbnd  27495  pntpbnd2  27526  pnt  27553  brbtwn2  28885  ax5seglem3  28911  ax5seglem6  28914  axpaschlem  28920  axcontlem2  28945  axcontlem4  28947  crctcshwlkn0lem4  29793  wwlkbp  29821  clwwisshclwwslem  29996  hst1a  32200  stge0  32206  sthil  32216  neldifpr1  32515  f1mptrn  32619  cshwrnid  32949  fsumrp0cl  33009  fzo0pmtrlast  33068  wrdpmtrlast  33069  psgnfzto1stlem  33076  slmdsrg  33183  primefldchr  33274  fldgensdrg  33287  primefldgen1  33294  1arithidomlem1  33507  1arithidomlem2  33508  1arithidom  33509  elunitge0  33933  xrge0iifcnv  33967  xrge0iifcv  33968  xrge0iifiso  33969  rrextnlm  34037  rrextchr  34038  0elros  34204  0elsros  34211  voliune  34263  volfiniune  34264  bnj563  34776  bnj1212  34832  bnj1219  34833  bnj1366  34862  bnj1379  34863  bnj545  34928  bnj594  34945  bnj1118  35017  bnj1177  35039  bnj1190  35041  bnj1398  35067  bnj1417  35074  bnj1450  35083  bnj1312  35091  bnj1523  35104  pthhashvtx  35193  msrval  35603  mclsppslem  35648  dfon2lem1  35846  dfrdg2  35858  cntotbnd  37856  heiborlem5  37875  heiborlem6  37876  eqvrelsymrel  38715  atl0dm  39421  dalem-ccly  39804  stoweidlem60  46182  fourierdlem40  46269  fourierdlem78  46306  upgrimpthslem1  48031  usgrgrtrirex  48074  ackval40  48818