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  8280  smofvon2  8282  smofvon  8285  errel  8637  elunitrn  13369  lincmb01cmp  13397  iccf1o  13398  elfznn0  13522  elfzouz  13565  ef01bndlem  16095  sin01bnd  16096  cos01bnd  16097  sin01gt0  16101  cos01gt0  16102  sin02gt0  16103  gzcn  16846  mresspw  17496  drsprs  18211  ipodrscl  18446  subgrcl  19046  pmtrfconj  19380  pgpprm  19507  slwprm  19523  efgsdmi  19646  efgsrel  19648  efgs1b  19650  efgsp1  19651  efgsres  19652  efgsfo  19653  efgredlema  19654  efgredlemf  19655  efgredlemd  19658  efgredlemc  19659  efgredlem  19661  efgrelexlemb  19664  efgcpbllemb  19669  omndmnd  20040  rngabl  20075  srgcmn  20109  ringgrp  20158  irredcl  20344  subrngrcl  20468  sdrgrcl  20706  orngring  20779  lmodgrp  20802  lssss  20871  phllvec  21568  obsrcl  21662  locfintop  23437  fclstop  23927  tmdmnd  23991  tgpgrp  23994  trgtgp  24084  tdrgtrg  24089  ust0  24136  ngpgrp  24515  elii1  24859  elii2  24860  icopnfcnv  24868  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  oprpiece1res2  24878  phtpcer  24922  pcoval2  24944  pcoass  24952  clmlmod  24995  cphphl  25099  cphnlm  25100  cphsca  25107  bnnvc  25268  uc1pcl  26077  mon1pcl  26078  sinq12ge0  26445  cosq14ge0  26448  cosq34lt1  26464  cosord  26468  cos11  26470  recosf1o  26472  resinf1o  26473  efifo  26484  logrncn  26499  atanf  26818  atanneg  26845  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  areass  26897  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  brbtwn2  28885  ax5seglem1  28908  ax5seglem2  28909  ax5seglem3  28911  ax5seglem5  28913  ax5seglem6  28914  ax5seglem9  28917  ax5seg  28918  axbtwnid  28919  axpaschlem  28920  axpasch  28921  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  pthistrl  29703  clwwlkbp  29967  sticl  32197  hstcl  32199  slmdcmn  33181  rrextnrg  34035  rrextdrg  34036  rossspw  34203  srossspw  34210  eulerpartlemd  34400  eulerpartlemf  34404  eulerpartlemgvv  34410  eulerpartlemgu  34411  eulerpartlemgh  34412  eulerpartlemgs2  34414  eulerpartlemn  34415  bnj564  34777  bnj1366  34862  bnj545  34928  bnj548  34930  bnj558  34935  bnj570  34938  bnj580  34946  bnj929  34969  bnj998  34990  bnj1006  34993  bnj1190  35041  bnj1523  35104  msrval  35603  mthmpps  35647  eqvrelrefrel  38715  atllat  39420  stoweidlem60  46183  fourierdlem111  46340  modmknepk  47487  prproropf1o  47632  gpgedgvtx1  48187  arweutermc  49656