MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2bi Structured version   Unicode version

Theorem simp2bi 1004
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
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 194 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1001 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
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:  smodm  6915  erdm  7214  ixpfn  7372  winafp  8968  inar1  9046  inatsk  9049  tskuni  9054  grur1  9091  supmullem1  10400  supmullem2  10401  supmul  10402  eluzelz  10974  elfz3nn0  11592  cshco  12575  swrds2  12656  ef01bndlem  13579  sin01bnd  13580  cos01bnd  13581  sin01gt0  13585  bitsss  13733  smueqlem  13797  gznegcl  14107  gzcjcl  14108  gzaddcl  14109  gzmulcl  14110  gzabssqcl  14113  4sqlem4a  14123  cshwshashlem2  14234  structcnvcnv  14296  structfun  14297  xpsff1o  14617  mre1cl  14643  drsbn0  15218  subgss  15793  symgfixelsi  16051  psgnunilem5  16111  pgpgrp  16206  slwsubg  16222  efgs1b  16346  efgsp1  16347  efgsres  16348  efgredeu  16362  efgred2  16363  efgcpbllemb  16365  srgmgp  16726  rngmgp  16766  irrednu  16912  lmodrng  17071  lmodprop2d  17122  lssn0  17137  phlsrng  18178  ocvss  18213  obsss  18267  fclsfil  19708  tmdtps  19772  tgptmd  19775  trgrng  19870  tdrgdrng  19873  ngpms  20317  icopnfcnv  20639  xrhmeo  20643  oprpiece1res2  20649  phtpcer  20692  pcoval2  20713  pcoass  20721  clmsca  20762  cphsqrcl  20828  bncms  20980  itg2ge0  21339  uc1pn0  21743  mon1pn0  21744  sinq12ge0  22096  cosq14gt0  22098  cosq14ge0  22099  sinord  22116  recosf1o  22117  resinf1o  22118  logrnaddcl  22152  atanf  22401  atanneg  22428  atancj  22431  efiatan  22433  atanlogaddlem  22434  atanlogadd  22435  atanlogsub  22437  efiatan2  22438  2efiatan  22439  tanatan  22440  dvatan  22456  areambl  22478  rlimcnp  22485  emgt0  22526  harmoniclbnd  22528  harmonicbnd4  22530  2sqlem2  22829  2sqlem3  22831  dchrvmasumlem2  22873  dchrvmasumiflem1  22876  logdivbnd  22931  pntpbnd2  22962  pnt  22989  brbtwn2  23296  ax5seglem3  23322  ax5seglem6  23325  axpaschlem  23331  axcontlem2  23356  axcontlem4  23358  eengbas  23372  ebtwntg  23373  ecgrtg  23374  elntg  23375  subgores  23936  subgoid  23939  subgoinv  23940  subgoablo  23943  ghsubgolem  24002  hst1a  25767  stge0  25773  sthil  25783  fsumrp0cl  26296  omndtos  26306  lmodslmd  26358  slmdsrg  26361  orngogrp  26407  elunitge0  26467  xrge0iifcnv  26501  xrge0iifcv  26502  xrge0iifiso  26503  rrextnlm  26570  rrextchr  26571  logbcl  26594  voliune  26782  volfiniune  26783  lgamgulmlem2  27153  dfon2lem1  27733  dfrdg2  27746  locfinbas  28714  cntotbnd  28836  heiborlem5  28855  heiborlem6  28856  stoweidlem60  29996  clwwisshclwwlem  30611  bnj563  32038  bnj1212  32096  bnj1219  32097  bnj1366  32126  bnj1379  32127  bnj545  32191  bnj594  32208  bnj1118  32278  bnj1177  32300  bnj1190  32302  bnj1398  32328  bnj1417  32335  bnj1450  32344  bnj1312  32352  bnj1523  32365  bj-flbi3  32836  atl0dm  33256  dalem-ccly  33638
  Copyright terms: Public domain W3C validator