Theorem simp2bi 1145

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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1142	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  smodm  8191  erdm  8517  ixpfn  8700  winafp  10462  inar1  10540  inatsk  10543  tskuni  10548  grur1  10585  supmullem1  11954  supmullem2  11955  supmul  11956  eluzelz  12601  elfz3nn0  13359  elfzo0l  13486  ico01fl0  13548  addmodlteq  13675  cshco  14558  swrds2  14662  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  bitsss  16142  smueqlem  16206  gznegcl  16645  gzcjcl  16646  gzaddcl  16647  gzmulcl  16648  gzabssqcl  16651  4sqlem4a  16661  cshwshashlem2  16807  structn0fun  16861  xpsff1o  17287  mre1cl  17312  drsbn0  18031  subgss  18765  symgfixelsi  19052  psgnunilem5  19111  pgpgrp  19208  slwsubg  19224  efgs1b  19351  efgsp1  19352  efgsres  19353  efgredeu  19367  efgred2  19368  efgcpbllemb  19370  srgmgp  19755  ringmgp  19798  irrednu  19956  sdrgint  20081  primefld  20082  primefld0cl  20083  primefld1cl  20084  lmodring  20140  lmodprop2d  20194  lssn0  20211  phlsrng  20845  ocvss  20884  obsss  20940  locfinbas  22682  fclsfil  23170  tmdtps  23236  tgptmd  23239  trgring  23331  tdrgdrng  23334  ngpms  23765  icopnfcnv  24114  xrhmeo  24118  oprpiece1res2  24124  phtpcer  24167  pcoval2  24188  pcoass  24196  clmsca  24237  cphsqrtcl  24357  bncms  24517  itg2ge0  24909  uc1pn0  25319  mon1pn0  25320  sinq12ge0  25674  cosq14gt0  25676  cosq14ge0  25677  cos02pilt1  25691  cosq34lt1  25692  sinord  25699  recosf1o  25700  resinf1o  25701  logrnaddcl  25739  logbcl  25926  relogbreexp  25934  atanf  26039  atanneg  26066  atancj  26069  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsub  26075  efiatan2  26076  2efiatan  26077  tanatan  26078  dvatan  26094  areambl  26117  rlimcnp  26124  emgt0  26165  harmoniclbnd  26167  harmonicbnd4  26169  lgamgulmlem2  26188  gausslemma2dlem1a  26522  2sqlem2  26575  2sqlem3  26577  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  logdivbnd  26713  pntpbnd2  26744  pnt  26771  brbtwn2  27282  ax5seglem3  27308  ax5seglem6  27311  axpaschlem  27317  axcontlem2  27342  axcontlem4  27344  crctcshwlkn0lem4  28187  wwlkbp  28215  clwwisshclwwslem  28387  hst1a  30589  stge0  30595  sthil  30605  neldifpr1  30890  f1mptrn  30979  cshwrnid  31242  fsumrp0cl  31313  omndtos  31340  psgnfzto1stlem  31376  slmdsrg  31469  primefldchr  31502  orngogrp  31509  elunitge0  31858  xrge0iifcnv  31892  xrge0iifcv  31893  xrge0iifiso  31894  rrextnlm  31962  rrextchr  31963  0elros  32147  0elsros  32154  voliune  32206  volfiniune  32207  bnj563  32732  bnj1212  32788  bnj1219  32789  bnj1366  32818  bnj1379  32819  bnj545  32884  bnj594  32901  bnj1118  32973  bnj1177  32995  bnj1190  32997  bnj1398  33023  bnj1417  33030  bnj1450  33039  bnj1312  33047  bnj1523  33060  pthhashvtx  33098  msrval  33509  mclsppslem  33554  dfon2lem1  33768  dfrdg2  33780  cntotbnd  35963  heiborlem5  35982  heiborlem6  35983  eqvrelsymrel  36719  atl0dm  37323  dalem-ccly  37706  stoweidlem60  43608  fourierdlem40  43695  fourierdlem78  43732  rngmgp  45447  ackval40  46050