Theorem simp1bi 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
simp1bi	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1bi

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

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

This theorem is referenced by:  limord  6372  smores2  8284  smofvon2  8286  smofvon  8289  errel  8641  elunitrn  13388  lincmb01cmp  13416  iccf1o  13417  elfznn0  13541  elfzouz  13584  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  cos01gt0  16118  sin02gt0  16119  gzcn  16862  mresspw  17512  drsprs  18227  ipodrscl  18462  subgrcl  19028  pmtrfconj  19363  pgpprm  19490  slwprm  19506  efgsdmi  19629  efgsrel  19631  efgs1b  19633  efgsp1  19634  efgsres  19635  efgsfo  19636  efgredlema  19637  efgredlemf  19638  efgredlemd  19641  efgredlemc  19642  efgredlem  19644  efgrelexlemb  19647  efgcpbllemb  19652  omndmnd  20023  rngabl  20058  srgcmn  20092  ringgrp  20141  irredcl  20327  subrngrcl  20454  sdrgrcl  20692  orngring  20765  lmodgrp  20788  lssss  20857  phllvec  21554  obsrcl  21648  locfintop  23424  fclstop  23914  tmdmnd  23978  tgpgrp  23981  trgtgp  24071  tdrgtrg  24076  ust0  24123  ngpgrp  24503  elii1  24847  elii2  24848  icopnfcnv  24856  icopnfhmeo  24857  iccpnfhmeo  24859  xrhmeo  24860  oprpiece1res2  24866  phtpcer  24910  pcoval2  24932  pcoass  24940  clmlmod  24983  cphphl  25087  cphnlm  25088  cphsca  25095  bnnvc  25256  uc1pcl  26065  mon1pcl  26066  sinq12ge0  26433  cosq14ge0  26436  cosq34lt1  26452  cosord  26456  cos11  26458  recosf1o  26460  resinf1o  26461  efifo  26472  logrncn  26487  atanf  26806  atanneg  26833  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  areass  26885  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  brbtwn2  28868  ax5seglem1  28891  ax5seglem2  28892  ax5seglem3  28894  ax5seglem5  28896  ax5seglem6  28897  ax5seglem9  28900  ax5seg  28901  axbtwnid  28902  axpaschlem  28903  axpasch  28904  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  pthistrl  29686  clwwlkbp  29947  sticl  32177  hstcl  32179  slmdcmn  33157  rrextnrg  33967  rrextdrg  33968  rossspw  34135  srossspw  34142  eulerpartlemd  34333  eulerpartlemf  34337  eulerpartlemgvv  34343  eulerpartlemgu  34344  eulerpartlemgh  34345  eulerpartlemgs2  34347  eulerpartlemn  34348  bnj564  34710  bnj1366  34795  bnj545  34861  bnj548  34863  bnj558  34868  bnj570  34871  bnj580  34879  bnj929  34902  bnj998  34923  bnj1006  34926  bnj1190  34974  bnj1523  35037  msrval  35510  mthmpps  35554  eqvrelrefrel  38574  atllat  39278  stoweidlem60  46042  fourierdlem111  46199  modmknepk  47347  prproropf1o  47492  gpgedgvtx1  48047  arweutermc  49516