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  6804  erdm  7103  ixpfn  7261  winafp  8856  inar1  8934  inatsk  8937  tskuni  8942  grur1  8979  supmullem1  10288  supmullem2  10289  supmul  10290  eluzelz  10862  elfz3nn0  11474  cshco  12456  swrds2  12537  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  sin01gt0  13466  bitsss  13614  smueqlem  13678  gznegcl  13988  gzcjcl  13989  gzaddcl  13990  gzmulcl  13991  gzabssqcl  13994  4sqlem4a  14004  cshwshashlem2  14115  structcnvcnv  14177  structfun  14178  xpsff1o  14498  mre1cl  14524  drsbn0  15099  subgss  15673  symgfixelsi  15931  psgnunilem5  15991  pgpgrp  16084  slwsubg  16100  efgs1b  16224  efgsp1  16225  efgsres  16226  efgredeu  16240  efgred2  16241  efgcpbllemb  16243  srgmgp  16600  rngmgp  16639  irrednu  16785  lmodrng  16934  lmodprop2d  16985  lssn0  16999  phlsrng  18035  ocvss  18070  obsss  18124  fclsfil  19558  tmdtps  19622  tgptmd  19625  trgrng  19720  tdrgdrng  19723  ngpms  20167  icopnfcnv  20489  xrhmeo  20493  oprpiece1res2  20499  phtpcer  20542  pcoval2  20563  pcoass  20571  clmsca  20612  cphsqrcl  20678  bncms  20830  itg2ge0  21188  uc1pn0  21592  mon1pn0  21593  sinq12ge0  21945  cosq14gt0  21947  cosq14ge0  21948  sinord  21965  recosf1o  21966  resinf1o  21967  logrnaddcl  22001  atanf  22250  atanneg  22277  atancj  22280  efiatan  22282  atanlogaddlem  22283  atanlogadd  22284  atanlogsub  22286  efiatan2  22287  2efiatan  22288  tanatan  22289  dvatan  22305  areambl  22327  rlimcnp  22334  emgt0  22375  harmoniclbnd  22377  harmonicbnd4  22379  2sqlem2  22678  2sqlem3  22680  dchrvmasumlem2  22722  dchrvmasumiflem1  22725  logdivbnd  22780  pntpbnd2  22811  pnt  22838  brbtwn2  23102  ax5seglem3  23128  ax5seglem6  23131  axpaschlem  23137  axcontlem2  23162  axcontlem4  23164  eengbas  23178  ebtwntg  23179  ecgrtg  23180  elntg  23181  subgores  23742  subgoid  23745  subgoinv  23746  subgoablo  23749  ghsubgolem  23808  hst1a  25573  stge0  25579  sthil  25589  fsumrp0cl  26109  omndtos  26119  lmodslmd  26171  slmdsrg  26174  orngogrp  26220  elunitge0  26281  xrge0iifcnv  26315  xrge0iifcv  26316  xrge0iifiso  26317  rrextnlm  26384  rrextchr  26385  logbcl  26408  voliune  26597  volfiniune  26598  lgamgulmlem2  26968  dfon2lem1  27547  dfrdg2  27560  locfinbas  28526  cntotbnd  28648  heiborlem5  28667  heiborlem6  28668  stoweidlem60  29808  clwwisshclwwlem  30423  bnj563  31622  bnj1212  31680  bnj1219  31681  bnj1366  31710  bnj1379  31711  bnj545  31775  bnj594  31792  bnj1118  31862  bnj1177  31884  bnj1190  31886  bnj1398  31912  bnj1417  31919  bnj1450  31928  bnj1312  31936  bnj1523  31949  bj-flbi3  32374  atl0dm  32787  dalem-ccly  33169
  Copyright terms: Public domain W3C validator