Theorem simp1bi 1024

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 199	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 1021	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 189   /\ w3a 986

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 190  df-an 377  df-3an 988

This theorem is referenced by:  limord  5461  smores2  7060  smofvon2  7062  smofvon  7065  errel  7359  lincmb01cmp  11766  iccf1o  11767  elfznn0  11878  elfzouz  11917  ef01bndlem  14249  sin01bnd  14250  cos01bnd  14251  sin01gt0  14255  cos01gt0  14256  sin02gt0  14257  gzcn  14887  mresspw  15509  drsprs  16192  ipodrscl  16419  subgrcl  16833  pmtrfconj  17118  pgpprm  17256  slwprm  17272  efgsdmi  17393  efgsrel  17395  efgs1b  17397  efgsp1  17398  efgsres  17399  efgsfo  17400  efgredlema  17401  efgredlemf  17402  efgredlemd  17405  efgredlemc  17406  efgredlem  17408  efgrelexlemb  17411  efgcpbllemb  17416  srgcmn  17753  ringgrp  17796  irredcl  17943  lmodgrp  18109  lssss  18171  phllvec  19207  obsrcl  19297  locfintop  20547  fclstop  21037  tmdmnd  21101  tgpgrp  21104  trgtgp  21193  tdrgtrg  21198  ust0  21245  ngpgrp  21624  elii1  21974  elii2  21975  icopnfcnv  21981  icopnfhmeo  21982  iccpnfhmeo  21984  xrhmeo  21985  oprpiece1res1  21990  oprpiece1res2  21991  phtpcer  22037  pcoval2  22058  pcoass  22066  clmlmod  22109  cphphl  22160  cphnlm  22161  cphsca  22168  bnnvc  22319  uc1pcl  23106  mon1pcl  23107  sinq12ge0  23475  cosq14ge0  23478  cosord  23493  cos11  23494  recosf1o  23496  resinf1o  23497  efifo  23508  logrncn  23524  atanf  23818  atanneg  23845  efiatan  23850  atanlogaddlem  23851  atanlogadd  23852  atanlogsub  23854  efiatan2  23855  2efiatan  23856  tanatan  23857  areass  23897  dchrvmasumlem2  24348  dchrvmasumiflem1  24351  brbtwn2  24947  ax5seglem1  24970  ax5seglem2  24971  ax5seglem3  24973  ax5seglem5  24975  ax5seglem6  24976  ax5seglem9  24979  ax5seg  24980  axbtwnid  24981  axpaschlem  24982  axpasch  24983  axcontlem2  25007  axcontlem4  25009  axcontlem7  25012  2spotiundisj  25802  subgores  26044  subgoid  26047  subgoinv  26048  sticl  27880  hstcl  27882  omndmnd  28474  slmdcmn  28528  orngring  28570  elunitrn  28710  rrextnrg  28812  rrextdrg  28813  rossspw  28998  srossspw  29005  eulerpartlemd  29205  eulerpartlemf  29209  eulerpartlemgvv  29215  eulerpartlemgu  29216  eulerpartlemgh  29217  eulerpartlemgs2  29219  eulerpartlemn  29220  bnj564  29560  bnj1366  29647  bnj545  29712  bnj548  29714  bnj558  29719  bnj570  29722  bnj580  29730  bnj929  29753  bnj998  29773  bnj1006  29776  bnj1190  29823  bnj1523  29886  msrval  30182  mthmpps  30226  atllat  32868  stoweidlem60  37978  fourierdlem111  38138  rngabl  40202