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:  smodm  8363  erdm  8727  ixpfn  8915  winafp  10709  inar1  10787  inatsk  10790  tskuni  10795  grur1  10832  supmullem1  12210  supmullem2  12211  supmul  12212  eluzelz  12860  elfz3nn0  13636  elfzo0l  13770  ico01fl0  13834  addmodlteq  13962  cshco  14853  swrds2  14957  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  bitsss  16443  smueqlem  16507  gznegcl  16953  gzcjcl  16954  gzaddcl  16955  gzmulcl  16956  gzabssqcl  16959  4sqlem4a  16969  cshwshashlem2  17114  structn0fun  17168  xpsff1o  17579  mre1cl  17604  drsbn0  18314  subgss  19108  symgfixelsi  19414  psgnunilem5  19473  pgpgrp  19573  slwsubg  19589  efgs1b  19715  efgsp1  19716  efgsres  19717  efgredeu  19731  efgred2  19732  efgcpbllemb  19734  rngmgp  20114  srgmgp  20149  ringmgp  20197  irrednu  20383  sdrgsubrg  20749  fldsdrgfld  20756  sdrgint  20762  primefld  20763  primefld0cl  20764  primefld1cl  20765  lmodring  20823  lmodprop2d  20879  lssn0  20895  phlsrng  21589  ocvss  21628  obsss  21682  locfinbas  23458  fclsfil  23946  tmdtps  24012  tgptmd  24015  trgring  24107  tdrgdrng  24110  ngpms  24537  icopnfcnv  24889  xrhmeo  24893  oprpiece1res2  24899  phtpcer  24943  pcoval2  24965  pcoass  24973  clmsca  25014  cphsqrtcl  25134  bncms  25294  itg2ge0  25686  uc1pn0  26101  mon1pn0  26102  sinq12ge0  26467  cosq14gt0  26469  cosq14ge0  26470  cos02pilt1  26485  cosq34lt1  26486  sinord  26493  recosf1o  26494  resinf1o  26495  logrnaddcl  26533  logbcl  26727  relogbreexp  26735  atanf  26840  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  dvatan  26895  areambl  26918  rlimcnp  26925  emgt0  26967  harmoniclbnd  26969  harmonicbnd4  26971  lgamgulmlem2  26990  gausslemma2dlem1a  27326  2sqlem2  27379  2sqlem3  27381  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  logdivbnd  27517  pntpbnd2  27548  pnt  27575  brbtwn2  28830  ax5seglem3  28856  ax5seglem6  28859  axpaschlem  28865  axcontlem2  28890  axcontlem4  28892  crctcshwlkn0lem4  29741  wwlkbp  29769  clwwisshclwwslem  29941  hst1a  32145  stge0  32151  sthil  32161  neldifpr1  32460  f1mptrn  32559  cshwrnid  32883  fsumrp0cl  32962  omndtos  33019  fzo0pmtrlast  33049  wrdpmtrlast  33050  psgnfzto1stlem  33057  slmdsrg  33150  primefldchr  33241  fldgensdrg  33254  primefldgen1  33261  orngogrp  33269  1arithidomlem1  33496  1arithidomlem2  33497  1arithidom  33498  elunitge0  33876  xrge0iifcnv  33910  xrge0iifcv  33911  xrge0iifiso  33912  rrextnlm  33980  rrextchr  33981  0elros  34147  0elsros  34154  voliune  34206  volfiniune  34207  bnj563  34720  bnj1212  34776  bnj1219  34777  bnj1366  34806  bnj1379  34807  bnj545  34872  bnj594  34889  bnj1118  34961  bnj1177  34983  bnj1190  34985  bnj1398  35011  bnj1417  35018  bnj1450  35027  bnj1312  35035  bnj1523  35048  pthhashvtx  35096  msrval  35506  mclsppslem  35551  dfon2lem1  35747  dfrdg2  35759  cntotbnd  37766  heiborlem5  37785  heiborlem6  37786  eqvrelsymrel  38563  atl0dm  39266  dalem-ccly  39650  stoweidlem60  46037  fourierdlem40  46124  fourierdlem78  46161  upgrimpthslem1  47868  usgrgrtrirex  47910  ackval40  48621