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  6362  smores2  8268  smofvon2  8270  smofvon  8273  errel  8625  elunitrn  13358  lincmb01cmp  13386  iccf1o  13387  elfznn0  13511  elfzouz  13554  ef01bndlem  16080  sin01bnd  16081  cos01bnd  16082  sin01gt0  16086  cos01gt0  16087  sin02gt0  16088  gzcn  16831  mresspw  17481  drsprs  18196  ipodrscl  18431  subgrcl  18997  pmtrfconj  19332  pgpprm  19459  slwprm  19475  efgsdmi  19598  efgsrel  19600  efgs1b  19602  efgsp1  19603  efgsres  19604  efgsfo  19605  efgredlema  19606  efgredlemf  19607  efgredlemd  19610  efgredlemc  19611  efgredlem  19613  efgrelexlemb  19616  efgcpbllemb  19621  omndmnd  19992  rngabl  20027  srgcmn  20061  ringgrp  20110  irredcl  20296  subrngrcl  20420  sdrgrcl  20658  orngring  20731  lmodgrp  20754  lssss  20823  phllvec  21520  obsrcl  21614  locfintop  23390  fclstop  23880  tmdmnd  23944  tgpgrp  23947  trgtgp  24037  tdrgtrg  24042  ust0  24089  ngpgrp  24468  elii1  24812  elii2  24813  icopnfcnv  24821  icopnfhmeo  24822  iccpnfhmeo  24824  xrhmeo  24825  oprpiece1res2  24831  phtpcer  24875  pcoval2  24897  pcoass  24905  clmlmod  24948  cphphl  25052  cphnlm  25053  cphsca  25060  bnnvc  25221  uc1pcl  26030  mon1pcl  26031  sinq12ge0  26398  cosq14ge0  26401  cosq34lt1  26417  cosord  26421  cos11  26423  recosf1o  26425  resinf1o  26426  efifo  26437  logrncn  26452  atanf  26771  atanneg  26798  efiatan  26803  atanlogaddlem  26804  atanlogadd  26805  atanlogsub  26807  efiatan2  26808  2efiatan  26809  tanatan  26810  areass  26850  dchrvmasumlem2  27390  dchrvmasumiflem1  27393  brbtwn2  28837  ax5seglem1  28860  ax5seglem2  28861  ax5seglem3  28863  ax5seglem5  28865  ax5seglem6  28866  ax5seglem9  28869  ax5seg  28870  axbtwnid  28871  axpaschlem  28872  axpasch  28873  axcontlem2  28897  axcontlem4  28899  axcontlem7  28902  pthistrl  29655  clwwlkbp  29916  sticl  32146  hstcl  32148  slmdcmn  33142  rrextnrg  33982  rrextdrg  33983  rossspw  34150  srossspw  34157  eulerpartlemd  34347  eulerpartlemf  34351  eulerpartlemgvv  34357  eulerpartlemgu  34358  eulerpartlemgh  34359  eulerpartlemgs2  34361  eulerpartlemn  34362  bnj564  34724  bnj1366  34809  bnj545  34875  bnj548  34877  bnj558  34882  bnj570  34885  bnj580  34893  bnj929  34916  bnj998  34937  bnj1006  34940  bnj1190  34988  bnj1523  35051  msrval  35528  mthmpps  35572  eqvrelrefrel  38592  atllat  39296  stoweidlem60  46055  fourierdlem111  46212  modmknepk  47360  prproropf1o  47505  gpgedgvtx1  48060  arweutermc  49529