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  6423  smores2  8347  smofvon2  8349  smofvon  8352  errel  8710  elunitrn  13524  lincmb01cmp  13552  iccf1o  13553  elfznn0  13679  elfzouz  13723  ef01bndlem  16278  sin01bnd  16279  cos01bnd  16280  sin01gt0  16284  cos01gt0  16285  sin02gt0  16286  gzcn  17030  mresspw  17682  drsprs  18397  ipodrscl  18632  subgrcl  19260  pmtrfconj  19599  pgpprm  19726  slwprm  19742  efgsdmi  19865  efgsrel  19867  efgs1b  19869  efgsp1  19870  efgsres  19871  efgsfo  19872  efgredlema  19873  efgredlemf  19874  efgredlemd  19877  efgredlemc  19878  efgredlem  19880  efgrelexlemb  19883  efgcpbllemb  19888  omndmnd  20259  rngabl  20296  srgcmn  20334  ringgrp  20383  irredcl  20571  subrngrcl  20719  sdrgrcl  20961  orngring  21034  lmodgrp  21057  lssss  21126  phllvec  21848  obsrcl  21942  locfintop  23753  fclstop  24243  tmdmnd  24307  tgpgrp  24310  trgtgp  24400  tdrgtrg  24405  ust0  24452  ngpgrp  24831  elii1  25169  elii2  25170  icopnfcnv  25176  icopnfhmeo  25177  iccpnfhmeo  25179  xrhmeo  25180  oprpiece1res2  25186  phtpcer  25229  pcoval2  25250  pcoass  25258  clmlmod  25301  cphphl  25405  cphnlm  25406  cphsca  25413  bnnvc  25574  uc1pcl  26376  mon1pcl  26377  sinq12ge0  26753  cosq14ge0  26756  cosq34lt1  26772  cosord  26776  cos11  26778  recosf1o  26780  resinf1o  26781  efifo  26792  logrncn  26807  atanf  27125  atanneg  27152  efiatan  27157  atanlogaddlem  27158  atanlogadd  27159  atanlogsub  27161  efiatan2  27162  2efiatan  27163  tanatan  27164  areass  27204  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  brbtwn2  29370  ax5seglem1  29393  ax5seglem2  29394  ax5seglem3  29396  ax5seglem5  29398  ax5seglem6  29399  ax5seglem9  29402  ax5seg  29403  axbtwnid  29404  axpaschlem  29405  axpasch  29406  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  pthistrl  30195  clwwlkbp  30463  sticl  32704  hstcl  32706  slmdcmn  33653  rrextnrg  34519  rrextdrg  34520  rossspw  34688  srossspw  34695  eulerpartlemd  34885  eulerpartlemf  34889  eulerpartlemgvv  34895  eulerpartlemgu  34896  eulerpartlemgh  34897  eulerpartlemgs2  34899  eulerpartlemn  34900  bnj564  35262  bnj1366  35346  bnj545  35412  bnj548  35414  bnj558  35419  bnj570  35422  bnj580  35430  bnj929  35453  bnj998  35474  bnj1006  35477  bnj1190  35525  bnj1523  35588  msrval  36125  mthmpps  36169  eqvrelrefrel  39438  atllat  40181  stoweidlem60  46896  fourierdlem111  47053  modmknepk  48264  muldvdsfacgt  48282  prproropf1o  48415  gpgedgvtx1  48986  arweutermc  50464