Theorem simp1bi 1163

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1bi	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1160	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  limord  6445  smores2  8393  smofvon2  8395  smofvon  8398  errel  8758  elunitrn  13628  lincmb01cmp  13656  iccf1o  13657  elfznn0  13784  elfzouz  13828  ef01bndlem  16384  sin01bnd  16385  cos01bnd  16386  sin01gt0  16390  cos01gt0  16391  sin02gt0  16392  gzcn  17142  mresspw  17794  drsprs  18509  ipodrscl  18744  subgrcl  19373  pmtrfconj  19713  pgpprm  19840  slwprm  19856  efgsdmi  19979  efgsrel  19981  efgs1b  19983  efgsp1  19984  efgsres  19985  efgsfo  19986  efgredlema  19987  efgredlemf  19988  efgredlemd  19991  efgredlemc  19992  efgredlem  19994  efgrelexlemb  19997  efgcpbllemb  20002  omndmnd  20373  rngabl  20410  srgcmn  20448  ringgrp  20497  irredcl  20687  subrngrcl  20836  sdrgrcl  21079  orngring  21152  lmodgrp  21175  lssss  21244  phllvec  21968  obsrcl  22062  locfintop  23873  fclstop  24363  tmdmnd  24427  tgpgrp  24430  trgtgp  24520  tdrgtrg  24525  ust0  24572  ngpgrp  24951  elii1  25289  elii2  25290  icopnfcnv  25296  icopnfhmeo  25297  iccpnfhmeo  25299  xrhmeo  25300  oprpiece1res2  25306  phtpcer  25349  pcoval2  25370  pcoass  25378  clmlmod  25421  cphphl  25525  cphnlm  25526  cphsca  25533  bnnvc  25694  uc1pcl  26495  mon1pcl  26496  sinq12ge0  26870  cosq14ge0  26873  cosq34lt1  26888  cosord  26892  cos11  26894  recosf1o  26896  resinf1o  26897  efifo  26908  logrncn  26923  atanf  27241  atanneg  27268  efiatan  27273  atanlogaddlem  27274  atanlogadd  27275  atanlogsub  27277  efiatan2  27278  2efiatan  27279  tanatan  27280  areass  27320  dchrvmasumlem2  27858  dchrvmasumiflem1  27861  brbtwn2  29516  ax5seglem1  29539  ax5seglem2  29540  ax5seglem3  29542  ax5seglem5  29544  ax5seglem6  29545  ax5seglem9  29548  ax5seg  29549  axbtwnid  29550  axpaschlem  29551  axpasch  29552  axcontlem2  29576  axcontlem4  29578  axcontlem7  29581  pthistrl  30341  clwwlkbp  30609  sticl  32850  hstcl  32852  slmdcmn  33842  rrextnrg  34716  rrextdrg  34717  rossspw  34885  srossspw  34892  eulerpartlemd  35081  eulerpartlemf  35085  eulerpartlemgvv  35091  eulerpartlemgu  35092  eulerpartlemgh  35093  eulerpartlemgs2  35095  eulerpartlemn  35096  bnj564  35458  bnj1366  35542  bnj545  35608  bnj548  35610  bnj558  35615  bnj570  35618  bnj580  35626  bnj929  35649  bnj998  35670  bnj1006  35673  bnj1190  35721  bnj1523  35784  msrval  36483  mthmpps  36527  eqvrelrefrel  39817  atllat  40560  dmstructnn  46130  dmstructfi  46131  stoweidlem60  47285  fourierdlem111  47442  modmknepk  48653  muldvdsfacgt  48671  prproropf1o  48804  gpgedgvtx1  49375  arweutermc  50880