Theorem simp2bi 1147

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 1144	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  0ellim  6387  smodm  8291  erdm  8654  ixpfn  8851  winafp  10620  inar1  10698  inatsk  10701  tskuni  10706  grur1  10743  supmullem1  12126  supmullem2  12127  supmul  12128  eluzelz  12798  elfz3nn0  13575  elfzo0l  13711  ico01fl0  13778  addmodlteq  13908  cshco  14798  swrds2  14902  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  bitsss  16395  smueqlem  16459  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  gzabssqcl  16912  4sqlem4a  16922  cshwshashlem2  17067  structn0fun  17121  xpsff1o  17531  mre1cl  17556  drsbn0  18270  subgss  19103  symgfixelsi  19410  psgnunilem5  19469  pgpgrp  19569  slwsubg  19585  efgs1b  19711  efgsp1  19712  efgsres  19713  efgredeu  19727  efgred2  19728  efgcpbllemb  19730  omndtos  20102  rngmgp  20137  srgmgp  20172  ringmgp  20220  irrednu  20405  sdrgsubrg  20768  fldsdrgfld  20775  sdrgint  20781  primefld  20782  primefld0cl  20783  primefld1cl  20784  orngogrp  20840  lmodring  20863  lmodprop2d  20919  lssn0  20935  phlsrng  21611  ocvss  21650  obsss  21704  locfinbas  23487  fclsfil  23975  tmdtps  24041  tgptmd  24044  trgring  24136  tdrgdrng  24139  ngpms  24565  icopnfcnv  24909  xrhmeo  24913  oprpiece1res2  24919  phtpcer  24962  pcoval2  24983  pcoass  24991  clmsca  25032  cphsqrtcl  25151  bncms  25311  itg2ge0  25702  uc1pn0  26111  mon1pn0  26112  sinq12ge0  26472  cosq14gt0  26474  cosq14ge0  26475  cos02pilt1  26490  cosq34lt1  26491  sinord  26498  recosf1o  26499  resinf1o  26500  logrnaddcl  26538  logbcl  26731  relogbreexp  26739  atanf  26844  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsub  26880  efiatan2  26881  2efiatan  26882  tanatan  26883  dvatan  26899  areambl  26922  rlimcnp  26929  emgt0  26970  harmoniclbnd  26972  harmonicbnd4  26974  lgamgulmlem2  26993  gausslemma2dlem1a  27328  2sqlem2  27381  2sqlem3  27383  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  logdivbnd  27519  pntpbnd2  27550  pnt  27577  brbtwn2  28974  ax5seglem3  29000  ax5seglem6  29003  axpaschlem  29009  axcontlem2  29034  axcontlem4  29036  crctcshwlkn0lem4  29881  wwlkbp  29909  clwwisshclwwslem  30084  hst1a  32289  stge0  32295  sthil  32305  neldifpr1  32603  f1mptrn  32708  cshwrnid  33021  fsumrp0cl  33081  fzo0pmtrlast  33153  wrdpmtrlast  33154  psgnfzto1stlem  33161  slmdsrg  33268  primefldchr  33362  fldgensdrg  33375  primefldgen1  33382  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  elunitge0  34043  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iifiso  34079  rrextnlm  34147  rrextchr  34148  0elros  34314  0elsros  34321  voliune  34373  volfiniune  34374  bnj563  34886  bnj1212  34941  bnj1219  34942  bnj1366  34971  bnj1379  34972  bnj545  35037  bnj594  35054  bnj1118  35126  bnj1177  35148  bnj1190  35150  bnj1398  35176  bnj1417  35183  bnj1450  35192  bnj1312  35200  bnj1523  35213  pthhashvtx  35310  msrval  35720  mclsppslem  35765  dfon2lem1  35963  dfrdg2  35975  cntotbnd  38117  heiborlem5  38136  heiborlem6  38137  eqvrelsymrel  39004  atl0dm  39748  dalem-ccly  40131  stoweidlem60  46488  fourierdlem40  46575  fourierdlem78  46612  upgrimpthslem1  48383  usgrgrtrirex  48426  ackval40  49169