Theorem simp1bi 1142

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

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

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 400  df-3an 1086

This theorem is referenced by:  limord  6218  smores2  7974  smofvon2  7976  smofvon  7979  errel  8281  elunitrn  12845  lincmb01cmp  12873  iccf1o  12874  elfznn0  12995  elfzouz  13037  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  gzcn  16258  mresspw  16855  drsprs  17538  ipodrscl  17764  subgrcl  18276  pmtrfconj  18586  pgpprm  18710  slwprm  18726  efgsdmi  18850  efgsrel  18852  efgs1b  18854  efgsp1  18855  efgsres  18856  efgsfo  18857  efgredlema  18858  efgredlemf  18859  efgredlemd  18862  efgredlemc  18863  efgredlem  18865  efgrelexlemb  18868  efgcpbllemb  18873  srgcmn  19251  ringgrp  19295  irredcl  19450  lmodgrp  19634  lssss  19701  phllvec  20318  obsrcl  20412  locfintop  22126  fclstop  22616  tmdmnd  22680  tgpgrp  22683  trgtgp  22773  tdrgtrg  22778  ust0  22825  ngpgrp  23205  elii1  23540  elii2  23541  icopnfcnv  23547  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  oprpiece1res2  23557  phtpcer  23600  pcoval2  23621  pcoass  23629  clmlmod  23672  cphphl  23776  cphnlm  23777  cphsca  23784  bnnvc  23944  uc1pcl  24744  mon1pcl  24745  sinq12ge0  25101  cosq14ge0  25104  cosq34lt1  25119  cosord  25123  cos11  25125  recosf1o  25127  resinf1o  25128  efifo  25139  logrncn  25154  atanf  25466  atanneg  25493  efiatan  25498  atanlogaddlem  25499  atanlogadd  25500  atanlogsub  25502  efiatan2  25503  2efiatan  25504  tanatan  25505  areass  25545  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  brbtwn2  26699  ax5seglem1  26722  ax5seglem2  26723  ax5seglem3  26725  ax5seglem5  26727  ax5seglem6  26728  ax5seglem9  26731  ax5seg  26732  axbtwnid  26733  axpaschlem  26734  axpasch  26735  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  pthistrl  27514  clwwlkbp  27770  sticl  29998  hstcl  30000  omndmnd  30755  slmdcmn  30883  orngring  30924  rrextnrg  31352  rrextdrg  31353  rossspw  31538  srossspw  31545  eulerpartlemd  31734  eulerpartlemf  31738  eulerpartlemgvv  31744  eulerpartlemgu  31745  eulerpartlemgh  31746  eulerpartlemgs2  31748  eulerpartlemn  31749  bnj564  32125  bnj1366  32211  bnj545  32277  bnj548  32279  bnj558  32284  bnj570  32287  bnj580  32295  bnj929  32318  bnj998  32339  bnj1006  32342  bnj1190  32390  bnj1523  32453  msrval  32898  mthmpps  32942  eqvrelrefrel  35993  atllat  36596  stoweidlem60  42702  fourierdlem111  42859  prproropf1o  44024  rngabl  44501