Theorem simp1bi 1146

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 1143	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  6444  smores2  8394  smofvon2  8396  smofvon  8399  errel  8754  elunitrn  13507  lincmb01cmp  13535  iccf1o  13536  elfznn0  13660  elfzouz  13703  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  gzcn  16970  mresspw  17635  drsprs  18349  ipodrscl  18583  subgrcl  19149  pmtrfconj  19484  pgpprm  19611  slwprm  19627  efgsdmi  19750  efgsrel  19752  efgs1b  19754  efgsp1  19755  efgsres  19756  efgsfo  19757  efgredlema  19758  efgredlemf  19759  efgredlemd  19762  efgredlemc  19763  efgredlem  19765  efgrelexlemb  19768  efgcpbllemb  19773  rngabl  20152  srgcmn  20186  ringgrp  20235  irredcl  20424  subrngrcl  20551  sdrgrcl  20790  lmodgrp  20865  lssss  20934  phllvec  21647  obsrcl  21743  locfintop  23529  fclstop  24019  tmdmnd  24083  tgpgrp  24086  trgtgp  24176  tdrgtrg  24181  ust0  24228  ngpgrp  24612  elii1  24964  elii2  24965  icopnfcnv  24973  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  oprpiece1res2  24983  phtpcer  25027  pcoval2  25049  pcoass  25057  clmlmod  25100  cphphl  25205  cphnlm  25206  cphsca  25213  bnnvc  25374  uc1pcl  26183  mon1pcl  26184  sinq12ge0  26550  cosq14ge0  26553  cosq34lt1  26569  cosord  26573  cos11  26575  recosf1o  26577  resinf1o  26578  efifo  26589  logrncn  26604  atanf  26923  atanneg  26950  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  areass  27002  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  brbtwn2  28920  ax5seglem1  28943  ax5seglem2  28944  ax5seglem3  28946  ax5seglem5  28948  ax5seglem6  28949  ax5seglem9  28952  ax5seg  28953  axbtwnid  28954  axpaschlem  28955  axpasch  28956  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  pthistrl  29743  clwwlkbp  30004  sticl  32234  hstcl  32236  omndmnd  33081  slmdcmn  33211  orngring  33330  rrextnrg  34002  rrextdrg  34003  rossspw  34170  srossspw  34177  eulerpartlemd  34368  eulerpartlemf  34372  eulerpartlemgvv  34378  eulerpartlemgu  34379  eulerpartlemgh  34380  eulerpartlemgs2  34382  eulerpartlemn  34383  bnj564  34758  bnj1366  34843  bnj545  34909  bnj548  34911  bnj558  34916  bnj570  34919  bnj580  34927  bnj929  34950  bnj998  34971  bnj1006  34974  bnj1190  35022  bnj1523  35085  msrval  35543  mthmpps  35587  eqvrelrefrel  38599  atllat  39301  stoweidlem60  46075  fourierdlem111  46232  prproropf1o  47494  gpgedgvtx1  48020  gpg3nbgrvtxlem  48023