Theorem simp1bi 1011

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 1008	1 |- ( ph -> ps )

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

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 371  df-3an 975

This theorem is referenced by:  limord  4937  smores2  7022  smofvon2  7024  smofvon  7027  errel  7317  lincmb01cmp  11659  iccf1o  11660  elfznn0  11766  elfzouz  11797  ef01bndlem  13776  sin01bnd  13777  cos01bnd  13778  sin01gt0  13782  cos01gt0  13783  sin02gt0  13784  smueqlem  13995  gzcn  14305  mresspw  14843  drsprs  15419  ipodrscl  15645  subgrcl  16001  pmtrfconj  16287  pgpprm  16409  slwprm  16425  efgsdmi  16546  efgsrel  16548  efgs1b  16550  efgsp1  16551  efgsres  16552  efgsfo  16553  efgredlema  16554  efgredlemf  16555  efgredlemd  16558  efgredlemc  16559  efgredlem  16561  efgrelexlemb  16564  efgcpbllemb  16569  srgcmn  16950  rnggrp  16991  irredcl  17137  lmodgrp  17302  lssss  17366  phllvec  18431  obsrcl  18521  fclstop  20247  tmdmnd  20309  tgpgrp  20312  trgtgp  20405  tdrgtrg  20410  ust0  20457  ngpgrp  20854  elii1  21170  elii2  21171  icopnfcnv  21177  icopnfhmeo  21178  iccpnfhmeo  21180  xrhmeo  21181  oprpiece1res1  21186  oprpiece1res2  21187  phtpcer  21230  pcoval2  21251  pcoass  21259  clmlmod  21302  cphphl  21353  cphnlm  21354  cphsca  21361  bnnvc  21514  uc1pcl  22279  mon1pcl  22280  sinq12ge0  22634  cosq14ge0  22637  cosord  22652  cos11  22653  recosf1o  22655  resinf1o  22656  efifo  22667  logrncn  22678  atanf  22939  atanneg  22966  efiatan  22971  atanlogaddlem  22972  atanlogadd  22973  atanlogsub  22975  efiatan2  22976  2efiatan  22977  tanatan  22978  areass  23017  dchrvmasumlem2  23411  dchrvmasumiflem1  23414  brbtwn2  23884  ax5seglem1  23907  ax5seglem2  23908  ax5seglem3  23910  ax5seglem5  23912  ax5seglem6  23913  ax5seglem9  23916  ax5seg  23917  axbtwnid  23918  axpaschlem  23919  axpasch  23920  axcontlem2  23944  axcontlem4  23946  axcontlem7  23949  2spotiundisj  24739  subgores  24982  subgoid  24985  subgoinv  24986  sticl  26810  hstcl  26812  omndmnd  27356  slmdcmn  27410  orngrng  27453  elunitrn  27515  rrextnrg  27618  rrextdrg  27619  eulerpartlemd  27945  eulerpartlemf  27949  eulerpartlemgvv  27955  eulerpartlemgu  27956  eulerpartlemgh  27957  eulerpartlemgs2  27959  eulerpartlemn  27960  locfintop  29772  stoweidlem60  31360  bnj564  32880  bnj1366  32967  bnj545  33032  bnj548  33034  bnj558  33039  bnj570  33042  bnj580  33050  bnj929  33073  bnj998  33093  bnj1006  33096  bnj1190  33143  bnj1523  33206  atllat  34097