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  4885  smores2  6924  smofvon2  6926  smofvon  6929  errel  7219  lincmb01cmp  11544  iccf1o  11545  elfznn0  11597  elfzouz  11673  ef01bndlem  13585  sin01bnd  13586  cos01bnd  13587  sin01gt0  13591  cos01gt0  13592  sin02gt0  13593  smueqlem  13803  gzcn  14110  mresspw  14648  drsprs  15224  ipodrscl  15450  subgrcl  15804  pmtrfconj  16090  pgpprm  16212  slwprm  16228  efgsdmi  16349  efgsrel  16351  efgs1b  16353  efgsp1  16354  efgsres  16355  efgsfo  16356  efgredlema  16357  efgredlemf  16358  efgredlemd  16361  efgredlemc  16362  efgredlem  16364  efgrelexlemb  16367  efgcpbllemb  16372  srgcmn  16731  rnggrp  16772  irredcl  16918  lmodgrp  17077  lssss  17140  phllvec  18182  obsrcl  18272  fclstop  19715  tmdmnd  19777  tgpgrp  19780  trgtgp  19873  tdrgtrg  19878  ust0  19925  ngpgrp  20322  elii1  20638  elii2  20639  icopnfcnv  20645  icopnfhmeo  20646  iccpnfhmeo  20648  xrhmeo  20649  oprpiece1res1  20654  oprpiece1res2  20655  phtpcer  20698  pcoval2  20719  pcoass  20727  clmlmod  20770  cphphl  20821  cphnlm  20822  cphsca  20829  bnnvc  20982  uc1pcl  21747  mon1pcl  21748  sinq12ge0  22102  cosq14ge0  22105  cosord  22120  cos11  22121  recosf1o  22123  resinf1o  22124  efifo  22135  logrncn  22146  atanf  22407  atanneg  22434  efiatan  22439  atanlogaddlem  22440  atanlogadd  22441  atanlogsub  22443  efiatan2  22444  2efiatan  22445  tanatan  22446  areass  22485  dchrvmasumlem2  22879  dchrvmasumiflem1  22882  brbtwn2  23302  ax5seglem1  23325  ax5seglem2  23326  ax5seglem3  23328  ax5seglem5  23330  ax5seglem6  23331  ax5seglem9  23334  ax5seg  23335  axbtwnid  23336  axpaschlem  23337  axpasch  23338  axcontlem2  23362  axcontlem4  23364  axcontlem7  23367  subgores  23942  subgoid  23945  subgoinv  23946  sticl  25770  hstcl  25772  omndmnd  26311  slmdcmn  26365  orngrng  26412  elunitrn  26471  rrextnrg  26574  rrextdrg  26575  eulerpartlemd  26892  eulerpartlemf  26896  eulerpartlemgvv  26902  eulerpartlemgu  26903  eulerpartlemgh  26904  eulerpartlemgs2  26906  eulerpartlemn  26907  locfintop  28719  stoweidlem60  30002  2spotiundisj  30802  bnj564  32053  bnj1366  32140  bnj545  32205  bnj548  32207  bnj558  32212  bnj570  32215  bnj580  32223  bnj929  32246  bnj998  32266  bnj1006  32269  bnj1190  32316  bnj1523  32379  atllat  33268