Theorem simp1bi 1009

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	|- ( ph <-> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
simp1bi	|- ( ph -> ps )

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 194	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 1006	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 971

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 185  df-an 369  df-3an 973

This theorem is referenced by:  limord  4926  smores2  7017  smofvon2  7019  smofvon  7022  errel  7312  lincmb01cmp  11666  iccf1o  11667  elfznn0  11775  elfzouz  11808  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  sin01gt0  14007  cos01gt0  14008  sin02gt0  14009  gzcn  14534  mresspw  15081  drsprs  15764  ipodrscl  15991  subgrcl  16405  pmtrfconj  16690  pgpprm  16812  slwprm  16828  efgsdmi  16949  efgsrel  16951  efgs1b  16953  efgsp1  16954  efgsres  16955  efgsfo  16956  efgredlema  16957  efgredlemf  16958  efgredlemd  16961  efgredlemc  16962  efgredlem  16964  efgrelexlemb  16967  efgcpbllemb  16972  srgcmn  17355  ringgrp  17398  irredcl  17548  lmodgrp  17714  lssss  17778  phllvec  18837  obsrcl  18927  locfintop  20188  fclstop  20678  tmdmnd  20740  tgpgrp  20743  trgtgp  20836  tdrgtrg  20841  ust0  20888  ngpgrp  21285  elii1  21601  elii2  21602  icopnfcnv  21608  icopnfhmeo  21609  iccpnfhmeo  21611  xrhmeo  21612  oprpiece1res1  21617  oprpiece1res2  21618  phtpcer  21661  pcoval2  21682  pcoass  21690  clmlmod  21733  cphphl  21784  cphnlm  21785  cphsca  21792  bnnvc  21945  uc1pcl  22710  mon1pcl  22711  sinq12ge0  23067  cosq14ge0  23070  cosord  23085  cos11  23086  recosf1o  23088  resinf1o  23089  efifo  23100  logrncn  23116  atanf  23408  atanneg  23435  efiatan  23440  atanlogaddlem  23441  atanlogadd  23442  atanlogsub  23444  efiatan2  23445  2efiatan  23446  tanatan  23447  areass  23487  dchrvmasumlem2  23881  dchrvmasumiflem1  23884  brbtwn2  24410  ax5seglem1  24433  ax5seglem2  24434  ax5seglem3  24436  ax5seglem5  24438  ax5seglem6  24439  ax5seglem9  24442  ax5seg  24443  axbtwnid  24444  axpaschlem  24445  axpasch  24446  axcontlem2  24470  axcontlem4  24472  axcontlem7  24475  2spotiundisj  25264  subgores  25504  subgoid  25507  subgoinv  25508  sticl  27332  hstcl  27334  omndmnd  27928  slmdcmn  27982  orngring  28025  elunitrn  28114  rrextnrg  28216  rrextdrg  28217  eulerpartlemd  28569  eulerpartlemf  28573  eulerpartlemgvv  28579  eulerpartlemgu  28580  eulerpartlemgh  28581  eulerpartlemgs2  28583  eulerpartlemn  28584  msrval  29162  mthmpps  29206  stoweidlem60  32081  fourierdlem111  32239  rngabl  32937  bnj564  34202  bnj1366  34289  bnj545  34354  bnj548  34356  bnj558  34361  bnj570  34364  bnj580  34372  bnj929  34395  bnj998  34415  bnj1006  34418  bnj1190  34465  bnj1523  34528  atllat  35422