Theorem simp1bi 1003

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

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

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 967

This theorem is referenced by:  limord  4773  smores2  6807  smofvon2  6809  smofvon  6812  errel  7102  lincmb01cmp  11420  iccf1o  11421  elfznn0  11473  elfzouz  11549  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  sin01gt0  13466  cos01gt0  13467  sin02gt0  13468  smueqlem  13678  gzcn  13985  mresspw  14522  drsprs  15098  ipodrscl  15324  subgrcl  15677  pmtrfconj  15963  pgpprm  16083  slwprm  16099  efgsdmi  16220  efgsrel  16222  efgs1b  16224  efgsp1  16225  efgsres  16226  efgsfo  16227  efgredlema  16228  efgredlemf  16229  efgredlemd  16232  efgredlemc  16233  efgredlem  16235  efgrelexlemb  16238  efgcpbllemb  16243  srgcmn  16598  rnggrp  16638  irredcl  16784  lmodgrp  16933  lssss  16995  phllvec  18033  obsrcl  18123  fclstop  19559  tmdmnd  19621  tgpgrp  19624  trgtgp  19717  tdrgtrg  19722  ust0  19769  ngpgrp  20166  elii1  20482  elii2  20483  icopnfcnv  20489  icopnfhmeo  20490  iccpnfhmeo  20492  xrhmeo  20493  oprpiece1res1  20498  oprpiece1res2  20499  phtpcer  20542  pcoval2  20563  pcoass  20571  clmlmod  20614  cphphl  20665  cphnlm  20666  cphsca  20673  bnnvc  20826  uc1pcl  21590  mon1pcl  21591  sinq12ge0  21945  cosq14ge0  21948  cosord  21963  cos11  21964  recosf1o  21966  resinf1o  21967  efifo  21978  logrncn  21989  atanf  22250  atanneg  22277  efiatan  22282  atanlogaddlem  22283  atanlogadd  22284  atanlogsub  22286  efiatan2  22287  2efiatan  22288  tanatan  22289  areass  22328  dchrvmasumlem2  22722  dchrvmasumiflem1  22725  brbtwn2  23102  ax5seglem1  23125  ax5seglem2  23126  ax5seglem3  23128  ax5seglem5  23130  ax5seglem6  23131  ax5seglem9  23134  ax5seg  23135  axbtwnid  23136  axpaschlem  23137  axpasch  23138  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  subgores  23742  subgoid  23745  subgoinv  23746  sticl  25570  hstcl  25572  omndmnd  26118  slmdcmn  26172  orngrng  26219  elunitrn  26279  rrextnrg  26382  rrextdrg  26383  eulerpartlemd  26701  eulerpartlemf  26705  eulerpartlemgvv  26711  eulerpartlemgu  26712  eulerpartlemgh  26713  eulerpartlemgs2  26715  eulerpartlemn  26716  locfintop  28525  stoweidlem60  29808  2spotiundisj  30608  bnj564  31623  bnj1366  31710  bnj545  31775  bnj548  31777  bnj558  31782  bnj570  31785  bnj580  31793  bnj929  31816  bnj998  31836  bnj1006  31839  bnj1190  31886  bnj1523  31949  atllat  32785