Theorem simp1bi 1020

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

Syntax hints:   -> wi 4   <-> wb 187   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  limord  5501  smores2  7081  smofvon2  7083  smofvon  7086  errel  7380  lincmb01cmp  11773  iccf1o  11774  elfznn0  11885  elfzouz  11922  ef01bndlem  14216  sin01bnd  14217  cos01bnd  14218  sin01gt0  14222  cos01gt0  14223  sin02gt0  14224  gzcn  14839  mresspw  15449  drsprs  16132  ipodrscl  16359  subgrcl  16773  pmtrfconj  17058  pgpprm  17180  slwprm  17196  efgsdmi  17317  efgsrel  17319  efgs1b  17321  efgsp1  17322  efgsres  17323  efgsfo  17324  efgredlema  17325  efgredlemf  17326  efgredlemd  17329  efgredlemc  17330  efgredlem  17332  efgrelexlemb  17335  efgcpbllemb  17340  srgcmn  17677  ringgrp  17720  irredcl  17867  lmodgrp  18033  lssss  18095  phllvec  19127  obsrcl  19217  locfintop  20467  fclstop  20957  tmdmnd  21021  tgpgrp  21024  trgtgp  21113  tdrgtrg  21118  ust0  21165  ngpgrp  21544  elii1  21859  elii2  21860  icopnfcnv  21866  icopnfhmeo  21867  iccpnfhmeo  21869  xrhmeo  21870  oprpiece1res1  21875  oprpiece1res2  21876  phtpcer  21919  pcoval2  21940  pcoass  21948  clmlmod  21991  cphphl  22042  cphnlm  22043  cphsca  22050  bnnvc  22201  uc1pcl  22969  mon1pcl  22970  sinq12ge0  23328  cosq14ge0  23331  cosord  23346  cos11  23347  recosf1o  23349  resinf1o  23350  efifo  23361  logrncn  23377  atanf  23671  atanneg  23698  efiatan  23703  atanlogaddlem  23704  atanlogadd  23705  atanlogsub  23707  efiatan2  23708  2efiatan  23709  tanatan  23710  areass  23750  dchrvmasumlem2  24199  dchrvmasumiflem1  24202  brbtwn2  24781  ax5seglem1  24804  ax5seglem2  24805  ax5seglem3  24807  ax5seglem5  24809  ax5seglem6  24810  ax5seglem9  24813  ax5seg  24814  axbtwnid  24815  axpaschlem  24816  axpasch  24817  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  2spotiundisj  25635  subgores  25877  subgoid  25880  subgoinv  25881  sticl  27703  hstcl  27705  omndmnd  28305  slmdcmn  28359  orngring  28402  elunitrn  28542  rrextnrg  28644  rrextdrg  28645  rossspw  28830  srossspw  28837  eulerpartlemd  29025  eulerpartlemf  29029  eulerpartlemgvv  29035  eulerpartlemgu  29036  eulerpartlemgh  29037  eulerpartlemgs2  29039  eulerpartlemn  29040  bnj564  29342  bnj1366  29429  bnj545  29494  bnj548  29496  bnj558  29501  bnj570  29504  bnj580  29512  bnj929  29535  bnj998  29555  bnj1006  29558  bnj1190  29605  bnj1523  29668  msrval  29964  mthmpps  30008  atllat  32575  stoweidlem60  37490  fourierdlem111  37649  rngabl  38635