Theorem simp2bi 1142

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

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

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 399  df-3an 1085

This theorem is referenced by:  smodm  7987  erdm  8298  ixpfn  8466  winafp  10118  inar1  10196  inatsk  10199  tskuni  10204  grur1  10241  supmullem1  11610  supmullem2  11611  supmul  11612  eluzelz  12252  elfz3nn0  13000  elfzo0l  13126  ico01fl0  13188  addmodlteq  13313  cshco  14197  swrds2  14301  ef01bndlem  15536  sin01bnd  15537  cos01bnd  15538  sin01gt0  15542  bitsss  15774  smueqlem  15838  gznegcl  16270  gzcjcl  16271  gzaddcl  16272  gzmulcl  16273  gzabssqcl  16276  4sqlem4a  16286  cshwshashlem2  16429  structn0fun  16494  xpsff1o  16839  mre1cl  16864  drsbn0  17546  subgss  18279  symgfixelsi  18562  psgnunilem5  18621  pgpgrp  18718  slwsubg  18734  efgs1b  18861  efgsp1  18862  efgsres  18863  efgredeu  18877  efgred2  18878  efgcpbllemb  18880  srgmgp  19259  ringmgp  19302  irrednu  19454  sdrgint  19582  primefld  19583  primefld0cl  19584  primefld1cl  19585  lmodring  19641  lmodprop2d  19695  lssn0  19711  phlsrng  20774  ocvss  20813  obsss  20867  locfinbas  22129  fclsfil  22617  tmdtps  22683  tgptmd  22686  trgring  22778  tdrgdrng  22781  ngpms  23208  icopnfcnv  23545  xrhmeo  23549  oprpiece1res2  23555  phtpcer  23598  pcoval2  23619  pcoass  23627  clmsca  23668  cphsqrtcl  23787  bncms  23946  itg2ge0  24335  uc1pn0  24738  mon1pn0  24739  sinq12ge0  25093  cosq14gt0  25095  cosq14ge0  25096  cos02pilt1  25110  cosq34lt1  25111  sinord  25117  recosf1o  25118  resinf1o  25119  logrnaddcl  25157  logbcl  25344  relogbreexp  25352  atanf  25457  atanneg  25484  atancj  25487  efiatan  25489  atanlogaddlem  25490  atanlogadd  25491  atanlogsub  25493  efiatan2  25494  2efiatan  25495  tanatan  25496  dvatan  25512  areambl  25535  rlimcnp  25542  emgt0  25583  harmoniclbnd  25585  harmonicbnd4  25587  lgamgulmlem2  25606  gausslemma2dlem1a  25940  2sqlem2  25993  2sqlem3  25995  dchrvmasumlem2  26073  dchrvmasumiflem1  26076  logdivbnd  26131  pntpbnd2  26162  pnt  26189  brbtwn2  26690  ax5seglem3  26716  ax5seglem6  26719  axpaschlem  26725  axcontlem2  26750  axcontlem4  26752  crctcshwlkn0lem4  27590  wwlkbp  27618  clwwisshclwwslem  27791  hst1a  29994  stge0  30000  sthil  30010  neldifpr1  30292  f1mptrn  30379  cshwrnid  30635  fsumrp0cl  30682  omndtos  30706  psgnfzto1stlem  30742  slmdsrg  30835  primefldchr  30867  orngogrp  30874  elunitge0  31142  xrge0iifcnv  31176  xrge0iifcv  31177  xrge0iifiso  31178  rrextnlm  31244  rrextchr  31245  0elros  31429  0elsros  31436  voliune  31488  volfiniune  31489  bnj563  32014  bnj1212  32071  bnj1219  32072  bnj1366  32101  bnj1379  32102  bnj545  32167  bnj594  32184  bnj1118  32256  bnj1177  32278  bnj1190  32280  bnj1398  32306  bnj1417  32313  bnj1450  32322  bnj1312  32330  bnj1523  32343  pthhashvtx  32374  msrval  32785  mclsppslem  32830  dfon2lem1  33028  dfrdg2  33040  cntotbnd  35073  heiborlem5  35092  heiborlem6  35093  eqvrelsymrel  35833  atl0dm  36437  dalem-ccly  36820  stoweidlem60  42344  fourierdlem40  42431  fourierdlem78  42468  rngmgp  44148