Theorem simp2bi 1077

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
simp2bi	|- ( ph -> ch )

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 206	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp2d 1074	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  smodm  7448  erdm  7752  ixpfn  7914  winafp  9519  inar1  9597  inatsk  9600  tskuni  9605  grur1  9642  supmullem1  10993  supmullem2  10994  supmul  10995  eluzelz  11697  elfz3nn0  12434  elfzo0l  12558  ico01fl0  12620  addmodlteq  12745  cshco  13582  swrds2  13685  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  bitsss  15148  smueqlem  15212  gznegcl  15639  gzcjcl  15640  gzaddcl  15641  gzmulcl  15642  gzabssqcl  15645  4sqlem4a  15655  cshwshashlem2  15803  structn0fun  15869  xpsff1o  16228  mre1cl  16254  drsbn0  16937  subgss  17595  symgfixelsi  17855  psgnunilem5  17914  pgpgrp  18009  slwsubg  18025  efgs1b  18149  efgsp1  18150  efgsres  18151  efgredeu  18165  efgred2  18166  efgcpbllemb  18168  srgmgp  18510  ringmgp  18553  irrednu  18705  lmodring  18871  lmodprop2d  18925  lssn0  18941  phlsrng  19976  ocvss  20014  obsss  20068  locfinbas  21325  fclsfil  21814  tmdtps  21880  tgptmd  21883  trgring  21974  tdrgdrng  21977  ngpms  22404  icopnfcnv  22741  xrhmeo  22745  oprpiece1res2  22751  phtpcer  22794  phtpcerOLD  22795  pcoval2  22816  pcoass  22824  clmsca  22865  cphsqrtcl  22984  bncms  23141  itg2ge0  23502  uc1pn0  23905  mon1pn0  23906  sinq12ge0  24260  cosq14gt0  24262  cosq14ge0  24263  sinord  24280  recosf1o  24281  resinf1o  24282  logrnaddcl  24321  logbcl  24505  relogbreexp  24513  atanf  24607  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  dvatan  24662  areambl  24685  rlimcnp  24692  emgt0  24733  harmoniclbnd  24735  harmonicbnd4  24737  lgamgulmlem2  24756  gausslemma2dlem1a  25090  2sqlem2  25143  2sqlem3  25145  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  logdivbnd  25245  pntpbnd2  25276  pnt  25303  brbtwn2  25785  ax5seglem3  25811  ax5seglem6  25814  axpaschlem  25820  axcontlem2  25845  axcontlem4  25847  eengbas  25861  ebtwntg  25862  ecgrtg  25863  elntg  25864  crctcshwlkn0lem4  26705  wwlkbp  26732  clwwisshclwwslem  26927  hst1a  29077  stge0  29083  sthil  29093  f1mptrn  29435  fsumrp0cl  29695  omndtos  29705  slmdsrg  29760  orngogrp  29801  psgnfzto1stlem  29850  elunitge0  29945  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iifiso  29981  rrextnlm  30047  rrextchr  30048  0elros  30233  0elsros  30240  voliune  30292  volfiniune  30293  bnj563  30813  bnj1212  30870  bnj1219  30871  bnj1366  30900  bnj1379  30901  bnj545  30965  bnj594  30982  bnj1118  31052  bnj1177  31074  bnj1190  31076  bnj1398  31102  bnj1417  31109  bnj1450  31118  bnj1312  31126  bnj1523  31139  msrval  31435  mclsppslem  31480  dfon2lem1  31688  dfrdg2  31701  cntotbnd  33595  heiborlem5  33614  heiborlem6  33615  atl0dm  34589  dalem-ccly  34971  elixpconstg  39266  stoweidlem60  40277  fourierdlem40  40364  fourierdlem78  40401  rngmgp  41878