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:  0ellim  6399  smodm  8323  erdm  8684  ixpfn  8879  winafp  10657  inar1  10735  inatsk  10738  tskuni  10743  grur1  10780  supmullem1  12160  supmullem2  12161  supmul  12162  eluzelz  12810  elfz3nn0  13589  elfzo0l  13724  ico01fl0  13788  addmodlteq  13918  cshco  14809  swrds2  14913  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  bitsss  16403  smueqlem  16467  gznegcl  16913  gzcjcl  16914  gzaddcl  16915  gzmulcl  16916  gzabssqcl  16919  4sqlem4a  16929  cshwshashlem2  17074  structn0fun  17128  xpsff1o  17537  mre1cl  17562  drsbn0  18272  subgss  19066  symgfixelsi  19372  psgnunilem5  19431  pgpgrp  19531  slwsubg  19547  efgs1b  19673  efgsp1  19674  efgsres  19675  efgredeu  19689  efgred2  19690  efgcpbllemb  19692  rngmgp  20072  srgmgp  20107  ringmgp  20155  irrednu  20341  sdrgsubrg  20707  fldsdrgfld  20714  sdrgint  20720  primefld  20721  primefld0cl  20722  primefld1cl  20723  lmodring  20781  lmodprop2d  20837  lssn0  20853  phlsrng  21547  ocvss  21586  obsss  21640  locfinbas  23416  fclsfil  23904  tmdtps  23970  tgptmd  23973  trgring  24065  tdrgdrng  24068  ngpms  24495  icopnfcnv  24847  xrhmeo  24851  oprpiece1res2  24857  phtpcer  24901  pcoval2  24923  pcoass  24931  clmsca  24972  cphsqrtcl  25091  bncms  25251  itg2ge0  25643  uc1pn0  26058  mon1pn0  26059  sinq12ge0  26424  cosq14gt0  26426  cosq14ge0  26427  cos02pilt1  26442  cosq34lt1  26443  sinord  26450  recosf1o  26451  resinf1o  26452  logrnaddcl  26490  logbcl  26684  relogbreexp  26692  atanf  26797  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  dvatan  26852  areambl  26875  rlimcnp  26882  emgt0  26924  harmoniclbnd  26926  harmonicbnd4  26928  lgamgulmlem2  26947  gausslemma2dlem1a  27283  2sqlem2  27336  2sqlem3  27338  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  logdivbnd  27474  pntpbnd2  27505  pnt  27532  brbtwn2  28839  ax5seglem3  28865  ax5seglem6  28868  axpaschlem  28874  axcontlem2  28899  axcontlem4  28901  crctcshwlkn0lem4  29750  wwlkbp  29778  clwwisshclwwslem  29950  hst1a  32154  stge0  32160  sthil  32170  neldifpr1  32469  f1mptrn  32566  cshwrnid  32890  fsumrp0cl  32969  omndtos  33026  fzo0pmtrlast  33056  wrdpmtrlast  33057  psgnfzto1stlem  33064  slmdsrg  33167  primefldchr  33258  fldgensdrg  33271  primefldgen1  33278  orngogrp  33286  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  elunitge0  33896  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iifiso  33932  rrextnlm  34000  rrextchr  34001  0elros  34167  0elsros  34174  voliune  34226  volfiniune  34227  bnj563  34740  bnj1212  34796  bnj1219  34797  bnj1366  34826  bnj1379  34827  bnj545  34892  bnj594  34909  bnj1118  34981  bnj1177  35003  bnj1190  35005  bnj1398  35031  bnj1417  35038  bnj1450  35047  bnj1312  35055  bnj1523  35068  pthhashvtx  35122  msrval  35532  mclsppslem  35577  dfon2lem1  35778  dfrdg2  35790  cntotbnd  37797  heiborlem5  37816  heiborlem6  37817  eqvrelsymrel  38597  atl0dm  39302  dalem-ccly  39686  stoweidlem60  46065  fourierdlem40  46152  fourierdlem78  46189  upgrimpthslem1  47911  usgrgrtrirex  47953  ackval40  48686