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  7084  smofvon2  7086  smofvon  7089  errel  7383  lincmb01cmp  11782  iccf1o  11783  elfznn0  11894  elfzouz  11931  ef01bndlem  14237  sin01bnd  14238  cos01bnd  14239  sin01gt0  14243  cos01gt0  14244  sin02gt0  14245  gzcn  14875  mresspw  15497  drsprs  16180  ipodrscl  16407  subgrcl  16821  pmtrfconj  17106  pgpprm  17244  slwprm  17260  efgsdmi  17381  efgsrel  17383  efgs1b  17385  efgsp1  17386  efgsres  17387  efgsfo  17388  efgredlema  17389  efgredlemf  17390  efgredlemd  17393  efgredlemc  17394  efgredlem  17396  efgrelexlemb  17399  efgcpbllemb  17404  srgcmn  17741  ringgrp  17784  irredcl  17931  lmodgrp  18097  lssss  18159  phllvec  19194  obsrcl  19284  locfintop  20534  fclstop  21024  tmdmnd  21088  tgpgrp  21091  trgtgp  21180  tdrgtrg  21185  ust0  21232  ngpgrp  21611  elii1  21961  elii2  21962  icopnfcnv  21968  icopnfhmeo  21969  iccpnfhmeo  21971  xrhmeo  21972  oprpiece1res1  21977  oprpiece1res2  21978  phtpcer  22024  pcoval2  22045  pcoass  22053  clmlmod  22096  cphphl  22147  cphnlm  22148  cphsca  22155  bnnvc  22306  uc1pcl  23092  mon1pcl  23093  sinq12ge0  23461  cosq14ge0  23464  cosord  23479  cos11  23480  recosf1o  23482  resinf1o  23483  efifo  23494  logrncn  23510  atanf  23804  atanneg  23831  efiatan  23836  atanlogaddlem  23837  atanlogadd  23838  atanlogsub  23840  efiatan2  23841  2efiatan  23842  tanatan  23843  areass  23883  dchrvmasumlem2  24334  dchrvmasumiflem1  24337  brbtwn2  24933  ax5seglem1  24956  ax5seglem2  24957  ax5seglem3  24959  ax5seglem5  24961  ax5seglem6  24962  ax5seglem9  24965  ax5seg  24966  axbtwnid  24967  axpaschlem  24968  axpasch  24969  axcontlem2  24993  axcontlem4  24995  axcontlem7  24998  2spotiundisj  25788  subgores  26030  subgoid  26033  subgoinv  26034  sticl  27866  hstcl  27868  omndmnd  28474  slmdcmn  28528  orngring  28571  elunitrn  28711  rrextnrg  28813  rrextdrg  28814  rossspw  28999  srossspw  29006  eulerpartlemd  29207  eulerpartlemf  29211  eulerpartlemgvv  29217  eulerpartlemgu  29218  eulerpartlemgh  29219  eulerpartlemgs2  29221  eulerpartlemn  29222  bnj564  29562  bnj1366  29649  bnj545  29714  bnj548  29716  bnj558  29721  bnj570  29724  bnj580  29732  bnj929  29755  bnj998  29775  bnj1006  29778  bnj1190  29825  bnj1523  29888  msrval  30184  mthmpps  30228  atllat  32835  stoweidlem60  37861  fourierdlem111  38021  rngabl  39496