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 1087

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 1089

This theorem is referenced by:  limord  6455  smores2  8410  smofvon2  8412  smofvon  8415  errel  8772  elunitrn  13527  lincmb01cmp  13555  iccf1o  13556  elfznn0  13677  elfzouz  13720  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  gzcn  16979  mresspw  17650  drsprs  18373  ipodrscl  18608  subgrcl  19171  pmtrfconj  19508  pgpprm  19635  slwprm  19651  efgsdmi  19774  efgsrel  19776  efgs1b  19778  efgsp1  19779  efgsres  19780  efgsfo  19781  efgredlema  19782  efgredlemf  19783  efgredlemd  19786  efgredlemc  19787  efgredlem  19789  efgrelexlemb  19792  efgcpbllemb  19797  rngabl  20182  srgcmn  20216  ringgrp  20265  irredcl  20450  subrngrcl  20577  sdrgrcl  20812  lmodgrp  20887  lssss  20957  phllvec  21670  obsrcl  21766  locfintop  23550  fclstop  24040  tmdmnd  24104  tgpgrp  24107  trgtgp  24197  tdrgtrg  24202  ust0  24249  ngpgrp  24633  elii1  24983  elii2  24984  icopnfcnv  24992  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  oprpiece1res2  25002  phtpcer  25046  pcoval2  25068  pcoass  25076  clmlmod  25119  cphphl  25224  cphnlm  25225  cphsca  25232  bnnvc  25393  uc1pcl  26203  mon1pcl  26204  sinq12ge0  26568  cosq14ge0  26571  cosq34lt1  26587  cosord  26591  cos11  26593  recosf1o  26595  resinf1o  26596  efifo  26607  logrncn  26622  atanf  26941  atanneg  26968  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  areass  27020  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  brbtwn2  28938  ax5seglem1  28961  ax5seglem2  28962  ax5seglem3  28964  ax5seglem5  28966  ax5seglem6  28967  ax5seglem9  28970  ax5seg  28971  axbtwnid  28972  axpaschlem  28973  axpasch  28974  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  pthistrl  29761  clwwlkbp  30017  sticl  32247  hstcl  32249  omndmnd  33054  slmdcmn  33184  orngring  33295  rrextnrg  33947  rrextdrg  33948  rossspw  34133  srossspw  34140  eulerpartlemd  34331  eulerpartlemf  34335  eulerpartlemgvv  34341  eulerpartlemgu  34342  eulerpartlemgh  34343  eulerpartlemgs2  34345  eulerpartlemn  34346  bnj564  34720  bnj1366  34805  bnj545  34871  bnj548  34873  bnj558  34878  bnj570  34881  bnj580  34889  bnj929  34912  bnj998  34933  bnj1006  34936  bnj1190  34984  bnj1523  35047  msrval  35506  mthmpps  35550  eqvrelrefrel  38554  atllat  39256  stoweidlem60  45981  fourierdlem111  46138  prproropf1o  47381