Theorem simp2bi 1158

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  0ellim  6406  smodm  8317  erdm  8684  ixpfn  8881  winafp  10652  inar1  10730  inatsk  10733  tskuni  10738  grur1  10775  supmullem1  12159  supmullem2  12160  supmul  12161  eluzelz  12846  elfz3nn0  13623  elfzo0l  13759  ico01fl0  13826  addmodlteq  13956  cshco  14846  swrds2  14950  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  sin01gt0  16205  bitsss  16443  smueqlem  16507  gznegcl  16954  gzcjcl  16955  gzaddcl  16956  gzmulcl  16957  gzabssqcl  16960  4sqlem4a  16970  cshwshashlem2  17115  structn0fun  17170  xpsff1o  17580  mre1cl  17605  drsbn0  18319  subgss  19152  symgfixelsi  19458  psgnunilem5  19517  pgpgrp  19617  slwsubg  19633  efgs1b  19759  efgsp1  19760  efgsres  19761  efgredeu  19775  efgred2  19776  efgcpbllemb  19778  omndtos  20150  rngmgp  20185  srgmgp  20220  ringmgp  20268  irrednu  20453  sdrgsubrg  20820  fldsdrgfld  20827  sdrgint  20833  primefld  20834  primefld0cl  20835  primefld1cl  20836  orngogrp  20892  lmodring  20915  lmodprop2d  20971  lssn0  20987  phlsrng  21663  ocvss  21702  obsss  21756  locfinbas  23562  fclsfil  24050  tmdtps  24116  tgptmd  24119  trgring  24211  tdrgdrng  24214  ngpms  24640  icopnfcnv  24984  xrhmeo  24988  oprpiece1res2  24994  phtpcer  25037  pcoval2  25058  pcoass  25066  clmsca  25107  cphsqrtcl  25226  bncms  25386  itg2ge0  25777  uc1pn0  26186  mon1pn0  26187  sinq12ge0  26550  cosq14gt0  26552  cosq14ge0  26553  cos02pilt1  26568  cosq34lt1  26569  sinord  26576  recosf1o  26577  resinf1o  26578  logrnaddcl  26616  logbcl  26809  relogbreexp  26817  atanf  26922  atanneg  26949  atancj  26952  efiatan  26954  atanlogaddlem  26955  atanlogadd  26956  atanlogsub  26958  efiatan2  26959  2efiatan  26960  tanatan  26961  dvatan  26977  areambl  27000  rlimcnp  27007  emgt0  27048  harmoniclbnd  27050  harmonicbnd4  27052  lgamgulmlem2  27071  gausslemma2dlem1a  27406  2sqlem2  27459  2sqlem3  27461  dchrvmasumlem2  27539  dchrvmasumiflem1  27542  logdivbnd  27597  pntpbnd2  27628  pnt  27655  brbtwn2  29052  ax5seglem3  29078  ax5seglem6  29081  axpaschlem  29087  axcontlem2  29112  axcontlem4  29114  crctcshwlkn0lem4  29959  wwlkbp  29987  clwwisshclwwslem  30162  hst1a  32367  stge0  32373  sthil  32383  neldifpr1  32681  f1mptrn  32787  cshwrnid  33100  fsumrp0cl  33160  fzo0pmtrlast  33233  wrdpmtrlast  33234  psgnfzto1stlem  33241  slmdsrg  33348  primefldchr  33449  fldgensdrg  33462  primefldgen1  33469  1arithidomlem1  33692  1arithidomlem2  33693  1arithidom  33694  elunitge0  34157  xrge0iifcnv  34191  xrge0iifcv  34192  xrge0iifiso  34193  rrextnlm  34261  rrextchr  34262  0elros  34428  0elsros  34435  voliune  34487  volfiniune  34488  bnj563  35003  bnj1212  35058  bnj1219  35059  bnj1366  35088  bnj1379  35089  bnj545  35154  bnj594  35171  bnj1118  35243  bnj1177  35265  bnj1190  35267  bnj1398  35293  bnj1417  35300  bnj1450  35309  bnj1312  35317  bnj1523  35330  pthhashvtx  35442  msrval  35852  mclsppslem  35897  dfon2lem1  36095  dfrdg2  36107  cntotbnd  38259  heiborlem5  38278  heiborlem6  38279  eqvrelsymrel  39146  atl0dm  39890  dalem-ccly  40273  stoweidlem60  46598  fourierdlem40  46685  fourierdlem78  46722  upgrimpthslem1  48493  usgrgrtrirex  48536  ackval40  49279