Theorem simp1bi 1012

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

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

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 976

This theorem is referenced by:  limord  4927  smores2  7027  smofvon2  7029  smofvon  7032  errel  7322  lincmb01cmp  11672  iccf1o  11673  elfznn0  11779  elfzouz  11812  ef01bndlem  13796  sin01bnd  13797  cos01bnd  13798  sin01gt0  13802  cos01gt0  13803  sin02gt0  13804  gzcn  14327  mresspw  14866  drsprs  15439  ipodrscl  15666  subgrcl  16080  pmtrfconj  16365  pgpprm  16487  slwprm  16503  efgsdmi  16624  efgsrel  16626  efgs1b  16628  efgsp1  16629  efgsres  16630  efgsfo  16631  efgredlema  16632  efgredlemf  16633  efgredlemd  16636  efgredlemc  16637  efgredlem  16639  efgrelexlemb  16642  efgcpbllemb  16647  srgcmn  17034  ringgrp  17077  irredcl  17227  lmodgrp  17393  lssss  17457  phllvec  18537  obsrcl  18627  locfintop  19895  fclstop  20385  tmdmnd  20447  tgpgrp  20450  trgtgp  20543  tdrgtrg  20548  ust0  20595  ngpgrp  20992  elii1  21308  elii2  21309  icopnfcnv  21315  icopnfhmeo  21316  iccpnfhmeo  21318  xrhmeo  21319  oprpiece1res1  21324  oprpiece1res2  21325  phtpcer  21368  pcoval2  21389  pcoass  21397  clmlmod  21440  cphphl  21491  cphnlm  21492  cphsca  21499  bnnvc  21652  uc1pcl  22417  mon1pcl  22418  sinq12ge0  22773  cosq14ge0  22776  cosord  22791  cos11  22792  recosf1o  22794  resinf1o  22795  efifo  22806  logrncn  22822  atanf  23083  atanneg  23110  efiatan  23115  atanlogaddlem  23116  atanlogadd  23117  atanlogsub  23119  efiatan2  23120  2efiatan  23121  tanatan  23122  areass  23161  dchrvmasumlem2  23555  dchrvmasumiflem1  23558  brbtwn2  24080  ax5seglem1  24103  ax5seglem2  24104  ax5seglem3  24106  ax5seglem5  24108  ax5seglem6  24109  ax5seglem9  24112  ax5seg  24113  axbtwnid  24114  axpaschlem  24115  axpasch  24116  axcontlem2  24140  axcontlem4  24142  axcontlem7  24145  2spotiundisj  24934  subgores  25178  subgoid  25181  subgoinv  25182  sticl  27006  hstcl  27008  omndmnd  27567  slmdcmn  27621  orngring  27663  elunitrn  27752  rrextnrg  27855  rrextdrg  27856  eulerpartlemd  28178  eulerpartlemf  28182  eulerpartlemgvv  28188  eulerpartlemgu  28189  eulerpartlemgh  28190  eulerpartlemgs2  28192  eulerpartlemn  28193  msrval  28771  mthmpps  28815  stoweidlem60  31731  fourierdlem111  31889  rngabl  32404  bnj564  33534  bnj1366  33621  bnj545  33686  bnj548  33688  bnj558  33693  bnj570  33696  bnj580  33704  bnj929  33727  bnj998  33747  bnj1006  33750  bnj1190  33797  bnj1523  33860  atllat  34765