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 1086

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 1088

This theorem is referenced by:  limord  6413  smores2  8366  smofvon2  8368  smofvon  8371  errel  8726  elunitrn  13482  lincmb01cmp  13510  iccf1o  13511  elfznn0  13635  elfzouz  13678  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  gzcn  16950  mresspw  17602  drsprs  18313  ipodrscl  18546  subgrcl  19112  pmtrfconj  19445  pgpprm  19572  slwprm  19588  efgsdmi  19711  efgsrel  19713  efgs1b  19715  efgsp1  19716  efgsres  19717  efgsfo  19718  efgredlema  19719  efgredlemf  19720  efgredlemd  19723  efgredlemc  19724  efgredlem  19726  efgrelexlemb  19729  efgcpbllemb  19734  rngabl  20113  srgcmn  20147  ringgrp  20196  irredcl  20382  subrngrcl  20509  sdrgrcl  20747  lmodgrp  20822  lssss  20891  phllvec  21587  obsrcl  21681  locfintop  23457  fclstop  23947  tmdmnd  24011  tgpgrp  24014  trgtgp  24104  tdrgtrg  24109  ust0  24156  ngpgrp  24536  elii1  24880  elii2  24881  icopnfcnv  24889  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  oprpiece1res2  24899  phtpcer  24943  pcoval2  24965  pcoass  24973  clmlmod  25016  cphphl  25121  cphnlm  25122  cphsca  25129  bnnvc  25290  uc1pcl  26099  mon1pcl  26100  sinq12ge0  26467  cosq14ge0  26470  cosq34lt1  26486  cosord  26490  cos11  26492  recosf1o  26494  resinf1o  26495  efifo  26506  logrncn  26521  atanf  26840  atanneg  26867  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  areass  26919  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  brbtwn2  28830  ax5seglem1  28853  ax5seglem2  28854  ax5seglem3  28856  ax5seglem5  28858  ax5seglem6  28859  ax5seglem9  28862  ax5seg  28863  axbtwnid  28864  axpaschlem  28865  axpasch  28866  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  pthistrl  29651  clwwlkbp  29912  sticl  32142  hstcl  32144  omndmnd  33018  slmdcmn  33148  orngring  33268  rrextnrg  33978  rrextdrg  33979  rossspw  34146  srossspw  34153  eulerpartlemd  34344  eulerpartlemf  34348  eulerpartlemgvv  34354  eulerpartlemgu  34355  eulerpartlemgh  34356  eulerpartlemgs2  34358  eulerpartlemn  34359  bnj564  34721  bnj1366  34806  bnj545  34872  bnj548  34874  bnj558  34879  bnj570  34882  bnj580  34890  bnj929  34913  bnj998  34934  bnj1006  34937  bnj1190  34985  bnj1523  35048  msrval  35506  mthmpps  35550  eqvrelrefrel  38562  atllat  39264  stoweidlem60  46037  fourierdlem111  46194  prproropf1o  47469  gpgedgvtx1  48014  gpg3nbgrvtxlem  48017  arweutermc  49363