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  6419  smores2  8344  smofvon2  8346  smofvon  8349  errel  8709  elunitrn  13523  lincmb01cmp  13551  iccf1o  13552  elfznn0  13678  elfzouz  13722  ef01bndlem  16275  sin01bnd  16276  cos01bnd  16277  sin01gt0  16281  cos01gt0  16282  sin02gt0  16283  gzcn  17027  mresspw  17679  drsprs  18394  ipodrscl  18629  subgrcl  19257  pmtrfconj  19596  pgpprm  19723  slwprm  19739  efgsdmi  19862  efgsrel  19864  efgs1b  19866  efgsp1  19867  efgsres  19868  efgsfo  19869  efgredlema  19870  efgredlemf  19871  efgredlemd  19874  efgredlemc  19875  efgredlem  19877  efgrelexlemb  19880  efgcpbllemb  19885  omndmnd  20256  rngabl  20293  srgcmn  20331  ringgrp  20380  irredcl  20568  subrngrcl  20716  sdrgrcl  20958  orngring  21031  lmodgrp  21054  lssss  21123  phllvec  21845  obsrcl  21939  locfintop  23750  fclstop  24240  tmdmnd  24304  tgpgrp  24307  trgtgp  24397  tdrgtrg  24402  ust0  24449  ngpgrp  24828  elii1  25166  elii2  25167  icopnfcnv  25173  icopnfhmeo  25174  iccpnfhmeo  25176  xrhmeo  25177  oprpiece1res2  25183  phtpcer  25226  pcoval2  25247  pcoass  25255  clmlmod  25298  cphphl  25402  cphnlm  25403  cphsca  25410  bnnvc  25571  uc1pcl  26372  mon1pcl  26373  sinq12ge0  26749  cosq14ge0  26752  cosq34lt1  26767  cosord  26771  cos11  26773  recosf1o  26775  resinf1o  26776  efifo  26787  logrncn  26802  atanf  27120  atanneg  27147  efiatan  27152  atanlogaddlem  27153  atanlogadd  27154  atanlogsub  27156  efiatan2  27157  2efiatan  27158  tanatan  27159  areass  27199  dchrvmasumlem2  27737  dchrvmasumiflem1  27740  brbtwn2  29365  ax5seglem1  29388  ax5seglem2  29389  ax5seglem3  29391  ax5seglem5  29393  ax5seglem6  29394  ax5seglem9  29397  ax5seg  29398  axbtwnid  29399  axpaschlem  29400  axpasch  29401  axcontlem2  29425  axcontlem4  29427  axcontlem7  29430  pthistrl  30190  clwwlkbp  30458  sticl  32699  hstcl  32701  slmdcmn  33648  rrextnrg  34514  rrextdrg  34515  rossspw  34683  srossspw  34690  eulerpartlemd  34880  eulerpartlemf  34884  eulerpartlemgvv  34890  eulerpartlemgu  34891  eulerpartlemgh  34892  eulerpartlemgs2  34894  eulerpartlemn  34895  bnj564  35257  bnj1366  35341  bnj545  35407  bnj548  35409  bnj558  35414  bnj570  35417  bnj580  35425  bnj929  35448  bnj998  35469  bnj1006  35472  bnj1190  35520  bnj1523  35583  msrval  36120  mthmpps  36164  eqvrelrefrel  39433  atllat  40176  stoweidlem60  46891  fourierdlem111  47048  modmknepk  48259  muldvdsfacgt  48277  prproropf1o  48410  gpgedgvtx1  48981  arweutermc  50459