Theorem simp1bi 1151

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 217	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1148	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  limord  6378  smores2  8291  smofvon2  8293  smofvon  8296  errel  8650  elunitrn  13418  lincmb01cmp  13446  iccf1o  13447  elfznn0  13572  elfzouz  13616  ef01bndlem  16149  sin01bnd  16150  cos01bnd  16151  sin01gt0  16155  cos01gt0  16156  sin02gt0  16157  gzcn  16901  mresspw  17552  drsprs  18267  ipodrscl  18502  subgrcl  19105  pmtrfconj  19439  pgpprm  19566  slwprm  19582  efgsdmi  19705  efgsrel  19707  efgs1b  19709  efgsp1  19710  efgsres  19711  efgsfo  19712  efgredlema  19713  efgredlemf  19714  efgredlemd  19717  efgredlemc  19718  efgredlem  19720  efgrelexlemb  19723  efgcpbllemb  19728  omndmnd  20099  rngabl  20134  srgcmn  20168  ringgrp  20217  irredcl  20402  subrngrcl  20530  sdrgrcl  20768  orngring  20841  lmodgrp  20864  lssss  20933  phllvec  21611  obsrcl  21705  locfintop  23511  fclstop  24001  tmdmnd  24065  tgpgrp  24068  trgtgp  24158  tdrgtrg  24163  ust0  24210  ngpgrp  24589  elii1  24927  elii2  24928  icopnfcnv  24934  icopnfhmeo  24935  iccpnfhmeo  24937  xrhmeo  24938  oprpiece1res2  24944  phtpcer  24987  pcoval2  25008  pcoass  25016  clmlmod  25059  cphphl  25163  cphnlm  25164  cphsca  25171  bnnvc  25332  uc1pcl  26134  mon1pcl  26135  sinq12ge0  26497  cosq14ge0  26500  cosq34lt1  26516  cosord  26520  cos11  26522  recosf1o  26524  resinf1o  26525  efifo  26536  logrncn  26551  atanf  26869  atanneg  26896  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsub  26905  efiatan2  26906  2efiatan  26907  tanatan  26908  areass  26948  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  brbtwn2  28999  ax5seglem1  29022  ax5seglem2  29023  ax5seglem3  29025  ax5seglem5  29027  ax5seglem6  29028  ax5seglem9  29031  ax5seg  29032  axbtwnid  29033  axpaschlem  29034  axpasch  29035  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  pthistrl  29816  clwwlkbp  30080  sticl  32311  hstcl  32313  slmdcmn  33293  rrextnrg  34192  rrextdrg  34193  rossspw  34360  srossspw  34367  eulerpartlemd  34557  eulerpartlemf  34561  eulerpartlemgvv  34567  eulerpartlemgu  34568  eulerpartlemgh  34569  eulerpartlemgs2  34571  eulerpartlemn  34572  bnj564  34934  bnj1366  35018  bnj545  35084  bnj548  35086  bnj558  35091  bnj570  35094  bnj580  35102  bnj929  35125  bnj998  35146  bnj1006  35149  bnj1190  35197  bnj1523  35260  msrval  35773  mthmpps  35817  eqvrelrefrel  39056  atllat  39799  stoweidlem60  46510  fourierdlem111  46667  modmknepk  47838  muldvdsfacgt  47856  prproropf1o  47989  gpgedgvtx1  48560  arweutermc  50027