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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  limord  6417  smores2  8346  smofvon2  8348  smofvon  8351  errel  8711  elunitrn  13579  lincmb01cmp  13607  iccf1o  13608  elfznn0  13734  elfzouz  13778  ef01bndlem  16332  sin01bnd  16333  cos01bnd  16334  sin01gt0  16338  cos01gt0  16339  sin02gt0  16340  gzcn  17090  mresspw  17742  drsprs  18457  ipodrscl  18692  subgrcl  19321  pmtrfconj  19660  pgpprm  19787  slwprm  19803  efgsdmi  19926  efgsrel  19928  efgs1b  19930  efgsp1  19931  efgsres  19932  efgsfo  19933  efgredlema  19934  efgredlemf  19935  efgredlemd  19938  efgredlemc  19939  efgredlem  19941  efgrelexlemb  19944  efgcpbllemb  19949  omndmnd  20320  rngabl  20357  srgcmn  20395  ringgrp  20444  irredcl  20634  subrngrcl  20783  sdrgrcl  21026  orngring  21099  lmodgrp  21122  lssss  21191  phllvec  21915  obsrcl  22009  locfintop  23820  fclstop  24310  tmdmnd  24374  tgpgrp  24377  trgtgp  24467  tdrgtrg  24472  ust0  24519  ngpgrp  24898  elii1  25236  elii2  25237  icopnfcnv  25243  icopnfhmeo  25244  iccpnfhmeo  25246  xrhmeo  25247  oprpiece1res2  25253  phtpcer  25296  pcoval2  25317  pcoass  25325  clmlmod  25368  cphphl  25472  cphnlm  25473  cphsca  25480  bnnvc  25641  uc1pcl  26442  mon1pcl  26443  sinq12ge0  26819  cosq14ge0  26822  cosq34lt1  26837  cosord  26841  cos11  26843  recosf1o  26845  resinf1o  26846  efifo  26857  logrncn  26872  atanf  27190  atanneg  27217  efiatan  27222  atanlogaddlem  27223  atanlogadd  27224  atanlogsub  27226  efiatan2  27227  2efiatan  27228  tanatan  27229  areass  27269  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  brbtwn2  29465  ax5seglem1  29488  ax5seglem2  29489  ax5seglem3  29491  ax5seglem5  29493  ax5seglem6  29494  ax5seglem9  29497  ax5seg  29498  axbtwnid  29499  axpaschlem  29500  axpasch  29501  axcontlem2  29525  axcontlem4  29527  axcontlem7  29530  pthistrl  30290  clwwlkbp  30558  sticl  32799  hstcl  32801  slmdcmn  33748  rrextnrg  34615  rrextdrg  34616  rossspw  34784  srossspw  34791  eulerpartlemd  34981  eulerpartlemf  34985  eulerpartlemgvv  34991  eulerpartlemgu  34992  eulerpartlemgh  34993  eulerpartlemgs2  34995  eulerpartlemn  34996  bnj564  35358  bnj1366  35442  bnj545  35508  bnj548  35510  bnj558  35515  bnj570  35518  bnj580  35526  bnj929  35549  bnj998  35570  bnj1006  35573  bnj1190  35621  bnj1523  35684  msrval  36272  mthmpps  36316  eqvrelrefrel  39582  atllat  40325  stoweidlem60  47014  fourierdlem111  47171  modmknepk  48382  muldvdsfacgt  48400  prproropf1o  48533  gpgedgvtx1  49104  arweutermc  50582