Theorem simp1bi 1141

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  limord  6250  smores2  7991  smofvon2  7993  smofvon  7996  errel  8298  lincmb01cmp  12882  iccf1o  12883  elfznn0  13001  elfzouz  13043  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  gzcn  16268  mresspw  16863  drsprs  17546  ipodrscl  17772  subgrcl  18284  pmtrfconj  18594  pgpprm  18718  slwprm  18734  efgsdmi  18858  efgsrel  18860  efgs1b  18862  efgsp1  18863  efgsres  18864  efgsfo  18865  efgredlema  18866  efgredlemf  18867  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgrelexlemb  18876  efgcpbllemb  18881  srgcmn  19258  ringgrp  19302  irredcl  19454  lmodgrp  19641  lssss  19708  phllvec  20773  obsrcl  20867  locfintop  22129  fclstop  22619  tmdmnd  22683  tgpgrp  22686  trgtgp  22776  tdrgtrg  22781  ust0  22828  ngpgrp  23208  elii1  23539  elii2  23540  icopnfcnv  23546  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  oprpiece1res2  23556  phtpcer  23599  pcoval2  23620  pcoass  23628  clmlmod  23671  cphphl  23775  cphnlm  23776  cphsca  23783  bnnvc  23943  uc1pcl  24737  mon1pcl  24738  sinq12ge0  25094  cosq14ge0  25097  cosq34lt1  25112  cosord  25116  cos11  25117  recosf1o  25119  resinf1o  25120  efifo  25131  logrncn  25146  atanf  25458  atanneg  25485  efiatan  25490  atanlogaddlem  25491  atanlogadd  25492  atanlogsub  25494  efiatan2  25495  2efiatan  25496  tanatan  25497  areass  25537  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  brbtwn2  26691  ax5seglem1  26714  ax5seglem2  26715  ax5seglem3  26717  ax5seglem5  26719  ax5seglem6  26720  ax5seglem9  26723  ax5seg  26724  axbtwnid  26725  axpaschlem  26726  axpasch  26727  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  pthistrl  27506  clwwlkbp  27763  sticl  29992  hstcl  29994  omndmnd  30705  slmdcmn  30833  orngring  30873  elunitrn  31140  rrextnrg  31242  rrextdrg  31243  rossspw  31428  srossspw  31435  eulerpartlemd  31624  eulerpartlemf  31628  eulerpartlemgvv  31634  eulerpartlemgu  31635  eulerpartlemgh  31636  eulerpartlemgs2  31638  eulerpartlemn  31639  bnj564  32015  bnj1366  32101  bnj545  32167  bnj548  32169  bnj558  32174  bnj570  32177  bnj580  32185  bnj929  32208  bnj998  32229  bnj1006  32232  bnj1190  32280  bnj1523  32343  msrval  32785  mthmpps  32829  eqvrelrefrel  35848  atllat  36451  stoweidlem60  42365  fourierdlem111  42522  prproropf1o  43689  rngabl  44168