Theorem simp1bi 1163

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  limord  6424  smores2  8342  smofvon2  8344  smofvon  8347  errel  8705  elunitrn  13495  lincmb01cmp  13523  iccf1o  13524  elfznn0  13650  elfzouz  13694  ef01bndlem  16241  sin01bnd  16242  cos01bnd  16243  sin01gt0  16247  cos01gt0  16248  sin02gt0  16249  gzcn  16993  mresspw  17645  drsprs  18360  ipodrscl  18595  subgrcl  19198  pmtrfconj  19537  pgpprm  19664  slwprm  19680  efgsdmi  19803  efgsrel  19805  efgs1b  19807  efgsp1  19808  efgsres  19809  efgsfo  19810  efgredlema  19811  efgredlemf  19812  efgredlemd  19815  efgredlemc  19816  efgredlem  19818  efgrelexlemb  19821  efgcpbllemb  19826  omndmnd  20197  rngabl  20234  srgcmn  20272  ringgrp  20321  irredcl  20507  subrngrcl  20637  sdrgrcl  20873  orngring  20946  lmodgrp  20969  lssss  21038  phllvec  21760  obsrcl  21854  locfintop  23659  fclstop  24149  tmdmnd  24213  tgpgrp  24216  trgtgp  24306  tdrgtrg  24311  ust0  24358  ngpgrp  24737  elii1  25075  elii2  25076  icopnfcnv  25082  icopnfhmeo  25083  iccpnfhmeo  25085  xrhmeo  25086  oprpiece1res2  25092  phtpcer  25135  pcoval2  25156  pcoass  25164  clmlmod  25207  cphphl  25311  cphnlm  25312  cphsca  25319  bnnvc  25480  uc1pcl  26282  mon1pcl  26283  sinq12ge0  26651  cosq14ge0  26654  cosq34lt1  26670  cosord  26674  cos11  26676  recosf1o  26678  resinf1o  26679  efifo  26690  logrncn  26705  atanf  27023  atanneg  27050  efiatan  27055  atanlogaddlem  27056  atanlogadd  27057  atanlogsub  27059  efiatan2  27060  2efiatan  27061  tanatan  27062  areass  27102  dchrvmasumlem2  27640  dchrvmasumiflem1  27643  brbtwn2  29233  ax5seglem1  29256  ax5seglem2  29257  ax5seglem3  29259  ax5seglem5  29261  ax5seglem6  29262  ax5seglem9  29265  ax5seg  29266  axbtwnid  29267  axpaschlem  29268  axpasch  29269  axcontlem2  29293  axcontlem4  29295  axcontlem7  29298  pthistrl  30050  clwwlkbp  30314  sticl  32545  hstcl  32547  slmdcmn  33503  rrextnrg  34369  rrextdrg  34370  rossspw  34537  srossspw  34544  eulerpartlemd  34734  eulerpartlemf  34738  eulerpartlemgvv  34744  eulerpartlemgu  34745  eulerpartlemgh  34746  eulerpartlemgs2  34748  eulerpartlemn  34749  bnj564  35111  bnj1366  35195  bnj545  35261  bnj548  35263  bnj558  35268  bnj570  35271  bnj580  35279  bnj929  35302  bnj998  35323  bnj1006  35326  bnj1190  35374  bnj1523  35437  msrval  36008  mthmpps  36052  eqvrelrefrel  39309  atllat  40052  stoweidlem60  46754  fourierdlem111  46911  modmknepk  48082  muldvdsfacgt  48100  prproropf1o  48233  gpgedgvtx1  48804  arweutermc  50285