Theorem simp2bi 1164

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 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1161	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  0ellim  6426  smodm  8344  erdm  8711  ixpfn  8914  winafp  10710  inar1  10788  inatsk  10791  tskuni  10796  grur1  10833  supmullem1  12213  supmullem2  12214  supmul  12215  eluzelz  12901  elfz3nn0  13680  elfzo0l  13816  ico01fl0  13884  addmodlteq  14014  cshco  14911  swrds2  15015  ef01bndlem  16278  sin01bnd  16279  cos01bnd  16280  sin01gt0  16284  bitsss  16522  smueqlem  16586  gznegcl  17033  gzcjcl  17034  gzaddcl  17035  gzmulcl  17036  gzabssqcl  17039  4sqlem4a  17049  cshwshashlem2  17194  structn0fun  17249  xpsff1o  17659  mre1cl  17684  drsbn0  18398  subgss  19256  symgfixelsi  19568  psgnunilem5  19627  pgpgrp  19727  slwsubg  19743  efgs1b  19869  efgsp1  19870  efgsres  19871  efgredeu  19885  efgred2  19886  efgcpbllemb  19888  omndtos  20260  rngmgp  20297  srgmgp  20336  ringmgp  20384  irrednu  20572  sdrgsubrg  20963  fldsdrgfld  20970  sdrgint  20976  primefld  20977  primefld0cl  20978  primefld1cl  20979  orngogrp  21035  lmodring  21058  lmodprop2d  21114  lssn0  21130  phlsrng  21850  ocvss  21889  obsss  21943  locfinbas  23754  fclsfil  24242  tmdtps  24308  tgptmd  24311  trgring  24403  tdrgdrng  24406  ngpms  24832  icopnfcnv  25176  xrhmeo  25180  oprpiece1res2  25186  phtpcer  25229  pcoval2  25250  pcoass  25258  clmsca  25299  cphsqrtcl  25418  bncms  25578  itg2ge0  25969  uc1pn0  26378  mon1pn0  26379  sinq12ge0  26753  cosq14gt0  26755  cosq14ge0  26756  cos02pilt1  26771  cosq34lt1  26772  sinord  26779  recosf1o  26780  resinf1o  26781  logrnaddcl  26819  logbcl  27012  relogbreexp  27020  atanf  27125  atanneg  27152  atancj  27155  efiatan  27157  atanlogaddlem  27158  atanlogadd  27159  atanlogsub  27161  efiatan2  27162  2efiatan  27163  tanatan  27164  dvatan  27180  areambl  27203  rlimcnp  27210  emgt0  27251  harmoniclbnd  27253  harmonicbnd4  27255  lgamgulmlem2  27274  gausslemma2dlem1a  27609  2sqlem2  27662  2sqlem3  27664  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  logdivbnd  27800  pntpbnd2  27831  pnt  27858  brbtwn2  29370  ax5seglem3  29396  ax5seglem6  29399  axpaschlem  29405  axcontlem2  29430  axcontlem4  29432  pthhashvtx  30202  crctcshwlkn0lem4  30289  wwlkbp  30317  clwwisshclwwslem  30492  hst1a  32707  stge0  32713  sthil  32723  neldifpr1  33016  f1mptrn  33116  cshwrnid  33409  fsumrp0cl  33469  fzo0pmtrlast  33540  wrdpmtrlast  33541  psgnfzto1stlem  33548  slmdsrg  33655  primefldchr  33750  fldgensdrg  33763  primefldgen1  33770  1arithidomlem1  33953  1arithidomlem2  33954  1arithidom  33955  elunitge0  34417  xrge0iifcnv  34451  xrge0iifcv  34452  xrge0iifiso  34453  rrextnlm  34521  rrextchr  34522  0elros  34689  0elsros  34696  voliune  34748  volfiniune  34749  bnj563  35261  bnj1212  35316  bnj1219  35317  bnj1366  35346  bnj1379  35347  bnj545  35412  bnj594  35429  bnj1118  35501  bnj1177  35523  bnj1190  35525  bnj1398  35551  bnj1417  35558  bnj1450  35567  bnj1312  35575  bnj1523  35588  msrval  36125  mclsppslem  36170  dfon2lem1  36368  dfrdg2  36380  cntotbnd  38554  heiborlem5  38573  heiborlem6  38574  eqvrelsymrel  39439  atl0dm  40183  dalem-ccly  40566  stoweidlem60  46896  fourierdlem40  46983  fourierdlem78  47020  upgrimpthslem1  48831  usgrgrtrirex  48874  ackval40  49631