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:  smodm  8391  erdm  8755  ixpfn  8943  winafp  10737  inar1  10815  inatsk  10818  tskuni  10823  grur1  10860  supmullem1  12238  supmullem2  12239  supmul  12240  eluzelz  12888  elfz3nn0  13661  elfzo0l  13795  ico01fl0  13859  addmodlteq  13987  cshco  14875  swrds2  14979  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  bitsss  16463  smueqlem  16527  gznegcl  16973  gzcjcl  16974  gzaddcl  16975  gzmulcl  16976  gzabssqcl  16979  4sqlem4a  16989  cshwshashlem2  17134  structn0fun  17188  xpsff1o  17612  mre1cl  17637  drsbn0  18350  subgss  19145  symgfixelsi  19453  psgnunilem5  19512  pgpgrp  19612  slwsubg  19628  efgs1b  19754  efgsp1  19755  efgsres  19756  efgredeu  19770  efgred2  19771  efgcpbllemb  19773  rngmgp  20153  srgmgp  20188  ringmgp  20236  irrednu  20425  sdrgsubrg  20792  fldsdrgfld  20799  sdrgint  20805  primefld  20806  primefld0cl  20807  primefld1cl  20808  lmodring  20866  lmodprop2d  20922  lssn0  20938  phlsrng  21649  ocvss  21688  obsss  21744  locfinbas  23530  fclsfil  24018  tmdtps  24084  tgptmd  24087  trgring  24179  tdrgdrng  24182  ngpms  24613  icopnfcnv  24973  xrhmeo  24977  oprpiece1res2  24983  phtpcer  25027  pcoval2  25049  pcoass  25057  clmsca  25098  cphsqrtcl  25218  bncms  25378  itg2ge0  25770  uc1pn0  26185  mon1pn0  26186  sinq12ge0  26550  cosq14gt0  26552  cosq14ge0  26553  cos02pilt1  26568  cosq34lt1  26569  sinord  26576  recosf1o  26577  resinf1o  26578  logrnaddcl  26616  logbcl  26810  relogbreexp  26818  atanf  26923  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  dvatan  26978  areambl  27001  rlimcnp  27008  emgt0  27050  harmoniclbnd  27052  harmonicbnd4  27054  lgamgulmlem2  27073  gausslemma2dlem1a  27409  2sqlem2  27462  2sqlem3  27464  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  logdivbnd  27600  pntpbnd2  27631  pnt  27658  brbtwn2  28920  ax5seglem3  28946  ax5seglem6  28949  axpaschlem  28955  axcontlem2  28980  axcontlem4  28982  crctcshwlkn0lem4  29833  wwlkbp  29861  clwwisshclwwslem  30033  hst1a  32237  stge0  32243  sthil  32253  neldifpr1  32551  f1mptrn  32645  cshwrnid  32946  fsumrp0cl  33026  omndtos  33082  fzo0pmtrlast  33112  wrdpmtrlast  33113  psgnfzto1stlem  33120  slmdsrg  33213  primefldchr  33303  fldgensdrg  33316  primefldgen1  33323  orngogrp  33331  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  elunitge0  33898  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iifiso  33934  rrextnlm  34004  rrextchr  34005  0elros  34171  0elsros  34178  voliune  34230  volfiniune  34231  bnj563  34757  bnj1212  34813  bnj1219  34814  bnj1366  34843  bnj1379  34844  bnj545  34909  bnj594  34926  bnj1118  34998  bnj1177  35020  bnj1190  35022  bnj1398  35048  bnj1417  35055  bnj1450  35064  bnj1312  35072  bnj1523  35085  pthhashvtx  35133  msrval  35543  mclsppslem  35588  dfon2lem1  35784  dfrdg2  35796  cntotbnd  37803  heiborlem5  37822  heiborlem6  37823  eqvrelsymrel  38600  atl0dm  39303  dalem-ccly  39687  stoweidlem60  46075  fourierdlem40  46162  fourierdlem78  46199  uspgrimprop  47873  usgrgrtrirex  47917  ackval40  48614