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

Theorem simp2bi 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
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 1009 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  smodm  7019  erdm  7318  ixpfn  7472  winafp  9071  inar1  9149  inatsk  9152  tskuni  9157  grur1  9194  supmullem1  10505  supmullem2  10506  supmul  10507  eluzelz  11087  elfz3nn0  11767  cshco  12761  swrds2  12842  ef01bndlem  13776  sin01bnd  13777  cos01bnd  13778  sin01gt0  13782  bitsss  13931  smueqlem  13995  gznegcl  14308  gzcjcl  14309  gzaddcl  14310  gzmulcl  14311  gzabssqcl  14314  4sqlem4a  14324  cshwshashlem2  14435  structcnvcnv  14497  structfun  14498  xpsff1o  14819  mre1cl  14845  drsbn0  15420  subgss  15997  symgfixelsi  16255  psgnunilem5  16315  pgpgrp  16410  slwsubg  16426  efgs1b  16550  efgsp1  16551  efgsres  16552  efgredeu  16566  efgred2  16567  efgcpbllemb  16569  srgmgp  16952  rngmgp  16992  irrednu  17138  lmodrng  17303  lmodprop2d  17355  lssn0  17370  phlsrng  18433  ocvss  18468  obsss  18522  fclsfil  20246  tmdtps  20310  tgptmd  20313  trgrng  20408  tdrgdrng  20411  ngpms  20855  icopnfcnv  21177  xrhmeo  21181  oprpiece1res2  21187  phtpcer  21230  pcoval2  21251  pcoass  21259  clmsca  21300  cphsqrtcl  21366  bncms  21518  itg2ge0  21877  uc1pn0  22281  mon1pn0  22282  sinq12ge0  22634  cosq14gt0  22636  cosq14ge0  22637  sinord  22654  recosf1o  22655  resinf1o  22656  logrnaddcl  22690  atanf  22939  atanneg  22966  atancj  22969  efiatan  22971  atanlogaddlem  22972  atanlogadd  22973  atanlogsub  22975  efiatan2  22976  2efiatan  22977  tanatan  22978  dvatan  22994  areambl  23016  rlimcnp  23023  emgt0  23064  harmoniclbnd  23066  harmonicbnd4  23068  2sqlem2  23367  2sqlem3  23369  dchrvmasumlem2  23411  dchrvmasumiflem1  23414  logdivbnd  23469  pntpbnd2  23500  pnt  23527  brbtwn2  23884  ax5seglem3  23910  ax5seglem6  23913  axpaschlem  23919  axcontlem2  23944  axcontlem4  23946  eengbas  23960  ebtwntg  23961  ecgrtg  23962  elntg  23963  clwwisshclwwlem  24482  subgores  24982  subgoid  24985  subgoinv  24986  subgoablo  24989  ghsubgolem  25048  hst1a  26813  stge0  26819  sthil  26829  fsumrp0cl  27347  omndtos  27357  lmodslmd  27409  slmdsrg  27412  orngogrp  27454  elunitge0  27517  xrge0iifcnv  27551  xrge0iifcv  27552  xrge0iifiso  27553  rrextnlm  27620  rrextchr  27621  logbcl  27653  voliune  27841  volfiniune  27842  lgamgulmlem2  28212  dfon2lem1  28792  dfrdg2  28805  locfinbas  29773  cntotbnd  29895  heiborlem5  29914  heiborlem6  29915  stoweidlem60  31360  fourierdlem40  31447  fourierdlem78  31485  bnj563  32879  bnj1212  32937  bnj1219  32938  bnj1366  32967  bnj1379  32968  bnj545  33032  bnj594  33049  bnj1118  33119  bnj1177  33141  bnj1190  33143  bnj1398  33169  bnj1417  33176  bnj1450  33185  bnj1312  33193  bnj1523  33206  bj-flbi3  33679  atl0dm  34099  dalem-ccly  34481
  Copyright terms: Public domain W3C validator