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  6396  smores2  8326  smofvon2  8328  smofvon  8331  errel  8683  elunitrn  13435  lincmb01cmp  13463  iccf1o  13464  elfznn0  13588  elfzouz  13631  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  gzcn  16910  mresspw  17560  drsprs  18271  ipodrscl  18504  subgrcl  19070  pmtrfconj  19403  pgpprm  19530  slwprm  19546  efgsdmi  19669  efgsrel  19671  efgs1b  19673  efgsp1  19674  efgsres  19675  efgsfo  19676  efgredlema  19677  efgredlemf  19678  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  efgrelexlemb  19687  efgcpbllemb  19692  rngabl  20071  srgcmn  20105  ringgrp  20154  irredcl  20340  subrngrcl  20467  sdrgrcl  20705  lmodgrp  20780  lssss  20849  phllvec  21545  obsrcl  21639  locfintop  23415  fclstop  23905  tmdmnd  23969  tgpgrp  23972  trgtgp  24062  tdrgtrg  24067  ust0  24114  ngpgrp  24494  elii1  24838  elii2  24839  icopnfcnv  24847  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  oprpiece1res2  24857  phtpcer  24901  pcoval2  24923  pcoass  24931  clmlmod  24974  cphphl  25078  cphnlm  25079  cphsca  25086  bnnvc  25247  uc1pcl  26056  mon1pcl  26057  sinq12ge0  26424  cosq14ge0  26427  cosq34lt1  26443  cosord  26447  cos11  26449  recosf1o  26451  resinf1o  26452  efifo  26463  logrncn  26478  atanf  26797  atanneg  26824  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  areass  26876  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  brbtwn2  28839  ax5seglem1  28862  ax5seglem2  28863  ax5seglem3  28865  ax5seglem5  28867  ax5seglem6  28868  ax5seglem9  28871  ax5seg  28872  axbtwnid  28873  axpaschlem  28874  axpasch  28875  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  pthistrl  29660  clwwlkbp  29921  sticl  32151  hstcl  32153  omndmnd  33025  slmdcmn  33165  orngring  33285  rrextnrg  33998  rrextdrg  33999  rossspw  34166  srossspw  34173  eulerpartlemd  34364  eulerpartlemf  34368  eulerpartlemgvv  34374  eulerpartlemgu  34375  eulerpartlemgh  34376  eulerpartlemgs2  34378  eulerpartlemn  34379  bnj564  34741  bnj1366  34826  bnj545  34892  bnj548  34894  bnj558  34899  bnj570  34902  bnj580  34910  bnj929  34933  bnj998  34954  bnj1006  34957  bnj1190  35005  bnj1523  35068  msrval  35532  mthmpps  35576  eqvrelrefrel  38596  atllat  39300  stoweidlem60  46065  fourierdlem111  46222  modmknepk  47367  prproropf1o  47512  gpgedgvtx1  48057  arweutermc  49523