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  6424  smores2  8365  smofvon2  8367  smofvon  8370  errel  8730  elunitrn  13601  lincmb01cmp  13629  iccf1o  13630  elfznn0  13757  elfzouz  13801  ef01bndlem  16357  sin01bnd  16358  cos01bnd  16359  sin01gt0  16363  cos01gt0  16364  sin02gt0  16365  gzcn  17115  mresspw  17767  drsprs  18482  ipodrscl  18717  subgrcl  19346  pmtrfconj  19685  pgpprm  19812  slwprm  19828  efgsdmi  19951  efgsrel  19953  efgs1b  19955  efgsp1  19956  efgsres  19957  efgsfo  19958  efgredlema  19959  efgredlemf  19960  efgredlemd  19963  efgredlemc  19964  efgredlem  19966  efgrelexlemb  19969  efgcpbllemb  19974  omndmnd  20345  rngabl  20382  srgcmn  20420  ringgrp  20469  irredcl  20659  subrngrcl  20808  sdrgrcl  21051  orngring  21124  lmodgrp  21147  lssss  21216  phllvec  21940  obsrcl  22034  locfintop  23845  fclstop  24335  tmdmnd  24399  tgpgrp  24402  trgtgp  24492  tdrgtrg  24497  ust0  24544  ngpgrp  24923  elii1  25261  elii2  25262  icopnfcnv  25268  icopnfhmeo  25269  iccpnfhmeo  25271  xrhmeo  25272  oprpiece1res2  25278  phtpcer  25321  pcoval2  25342  pcoass  25350  clmlmod  25393  cphphl  25497  cphnlm  25498  cphsca  25505  bnnvc  25666  uc1pcl  26467  mon1pcl  26468  sinq12ge0  26842  cosq14ge0  26845  cosq34lt1  26860  cosord  26864  cos11  26866  recosf1o  26868  resinf1o  26869  efifo  26880  logrncn  26895  atanf  27213  atanneg  27240  efiatan  27245  atanlogaddlem  27246  atanlogadd  27247  atanlogsub  27249  efiatan2  27250  2efiatan  27251  tanatan  27252  areass  27292  dchrvmasumlem2  27830  dchrvmasumiflem1  27833  brbtwn2  29488  ax5seglem1  29511  ax5seglem2  29512  ax5seglem3  29514  ax5seglem5  29516  ax5seglem6  29517  ax5seglem9  29520  ax5seg  29521  axbtwnid  29522  axpaschlem  29523  axpasch  29524  axcontlem2  29548  axcontlem4  29550  axcontlem7  29553  pthistrl  30313  clwwlkbp  30581  sticl  32822  hstcl  32824  slmdcmn  33812  rrextnrg  34679  rrextdrg  34680  rossspw  34848  srossspw  34855  eulerpartlemd  35044  eulerpartlemf  35048  eulerpartlemgvv  35054  eulerpartlemgu  35055  eulerpartlemgh  35056  eulerpartlemgs2  35058  eulerpartlemn  35059  bnj564  35421  bnj1366  35505  bnj545  35571  bnj548  35573  bnj558  35578  bnj570  35581  bnj580  35589  bnj929  35612  bnj998  35633  bnj1006  35636  bnj1190  35684  bnj1523  35747  msrval  36389  mthmpps  36433  eqvrelrefrel  39707  atllat  40450  dmstructnn  46019  dmstructfi  46020  stoweidlem60  47163  fourierdlem111  47320  modmknepk  48531  muldvdsfacgt  48549  prproropf1o  48682  gpgedgvtx1  49253  arweutermc  50758