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  6420  smodm  8343  erdm  8712  ixpfn  8915  winafp  10763  inar1  10841  inatsk  10844  tskuni  10849  grur1  10886  supmullem1  12268  supmullem2  12269  supmul  12270  eluzelz  12956  elfz3nn0  13735  elfzo0l  13871  ico01fl0  13939  addmodlteq  14069  cshco  14967  swrds2  15071  ef01bndlem  16332  sin01bnd  16333  cos01bnd  16334  sin01gt0  16338  bitsss  16576  smueqlem  16640  gznegcl  17093  gzcjcl  17094  gzaddcl  17095  gzmulcl  17096  gzabssqcl  17099  4sqlem4a  17109  cshwshashlem2  17254  structn0fun  17309  xpsff1o  17719  mre1cl  17744  drsbn0  18458  subgss  19317  symgfixelsi  19629  psgnunilem5  19688  pgpgrp  19788  slwsubg  19804  efgs1b  19930  efgsp1  19931  efgsres  19932  efgredeu  19946  efgred2  19947  efgcpbllemb  19949  omndtos  20321  rngmgp  20358  srgmgp  20397  ringmgp  20445  irrednu  20635  sdrgsubrg  21028  fldsdrgfld  21035  sdrgint  21041  primefld  21042  primefld0cl  21043  primefld1cl  21044  orngogrp  21100  lmodring  21123  lmodprop2d  21179  lssn0  21195  phlsrng  21917  ocvss  21956  obsss  22010  locfinbas  23821  fclsfil  24309  tmdtps  24375  tgptmd  24378  trgring  24470  tdrgdrng  24473  ngpms  24899  icopnfcnv  25243  xrhmeo  25247  oprpiece1res2  25253  phtpcer  25296  pcoval2  25317  pcoass  25325  clmsca  25366  cphsqrtcl  25485  bncms  25645  itg2ge0  26036  uc1pn0  26444  mon1pn0  26445  sinq12ge0  26819  cosq14gt0  26821  cosq14ge0  26822  cos02pilt1  26836  cosq34lt1  26837  sinord  26844  recosf1o  26845  resinf1o  26846  logrnaddcl  26884  logbcl  27077  relogbreexp  27085  atanf  27190  atanneg  27217  atancj  27220  efiatan  27222  atanlogaddlem  27223  atanlogadd  27224  atanlogsub  27226  efiatan2  27227  2efiatan  27228  tanatan  27229  dvatan  27245  areambl  27268  rlimcnp  27275  emgt0  27316  harmoniclbnd  27318  harmonicbnd4  27320  lgamgulmlem2  27339  gausslemma2dlem1a  27674  2sqlem2  27727  2sqlem3  27729  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  logdivbnd  27865  pntpbnd2  27896  pnt  27923  brbtwn2  29465  ax5seglem3  29491  ax5seglem6  29494  axpaschlem  29500  axcontlem2  29525  axcontlem4  29527  pthhashvtx  30297  crctcshwlkn0lem4  30384  wwlkbp  30412  clwwisshclwwslem  30587  hst1a  32802  stge0  32808  sthil  32818  neldifpr1  33111  f1mptrn  33211  cshwrnid  33504  fsumrp0cl  33564  fzo0pmtrlast  33635  wrdpmtrlast  33636  psgnfzto1stlem  33643  slmdsrg  33750  primefldchr  33845  fldgensdrg  33858  primefldgen1  33865  1arithidomlem1  34049  1arithidomlem2  34050  1arithidom  34051  elunitge0  34513  xrge0iifcnv  34547  xrge0iifcv  34548  xrge0iifiso  34549  rrextnlm  34617  rrextchr  34618  0elros  34785  0elsros  34792  voliune  34844  volfiniune  34845  bnj563  35357  bnj1212  35412  bnj1219  35413  bnj1366  35442  bnj1379  35443  bnj545  35508  bnj594  35525  bnj1118  35597  bnj1177  35619  bnj1190  35621  bnj1398  35647  bnj1417  35654  bnj1450  35663  bnj1312  35671  bnj1523  35684  msrval  36272  mclsppslem  36317  dfon2lem1  36515  dfrdg2  36527  cntotbnd  38698  heiborlem5  38717  heiborlem6  38718  eqvrelsymrel  39583  atl0dm  40327  dalem-ccly  40710  stoweidlem60  47014  fourierdlem40  47101  fourierdlem78  47138  upgrimpthslem1  48949  usgrgrtrirex  48992  ackval40  49749