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

Theorem simp2bi 973
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 187 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 970 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  smodm  6613  abianfplem  6715  erdm  6915  ixpfn  7068  winafp  8572  inar1  8650  inatsk  8653  tskuni  8658  grur1  8695  supmullem1  9974  supmullem2  9975  supmul  9976  eluzelz  10496  elfz3nn0  11084  swrds2  11880  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  sin01gt0  12791  bitsss  12938  smueqlem  13002  gznegcl  13303  gzcjcl  13304  gzaddcl  13305  gzmulcl  13306  gzabssqcl  13309  4sqlem4a  13319  structcnvcnv  13480  structfun  13481  xpsff1o  13793  mre1cl  13819  drsbn0  14394  subgss  14945  pgpgrp  15228  slwsubg  15244  efgs1b  15368  efgsp1  15369  efgsres  15370  efgredeu  15384  efgred2  15385  efgcpbllemb  15387  rngmgp  15670  irrednu  15810  lmodrng  15958  lmodprop2d  16006  lssn0  16017  phlsrng  16862  ocvss  16897  obsss  16951  fclsfil  18042  tmdtps  18106  tgptmd  18109  trgrng  18200  tdrgdrng  18203  ngpms  18647  icopnfcnv  18967  xrhmeo  18971  oprpiece1res2  18977  phtpcer  19020  pcoval2  19041  pcoass  19049  clmsca  19090  cphsqrcl  19147  bncms  19297  itg2ge0  19627  uc1pn0  20068  mon1pn0  20069  sinq12ge0  20416  cosq14gt0  20418  cosq14ge0  20419  sinord  20436  recosf1o  20437  resinf1o  20438  logrnaddcl  20472  atanf  20720  atanneg  20747  atancj  20750  efiatan  20752  atanlogaddlem  20753  atanlogadd  20754  atanlogsub  20756  efiatan2  20757  2efiatan  20758  tanatan  20759  dvatan  20775  areambl  20797  rlimcnp  20804  emgt0  20845  harmoniclbnd  20847  harmonicbnd4  20849  2sqlem2  21148  2sqlem3  21150  dchrvmasumlem2  21192  dchrvmasumiflem1  21195  logdivbnd  21250  pntpbnd2  21281  pnt  21308  subgores  21892  subgoid  21895  subgoinv  21896  subgoablo  21899  ghsubgolem  21958  hst1a  23721  stge0  23727  sthil  23737  fsumrp0cl  24217  ofldtos  24237  elunitge0  24297  xrge0iifcnv  24319  xrge0iifcv  24320  xrge0iifiso  24321  logbcl  24397  voliune  24585  volfiniune  24586  lgamgulmlem2  24814  dfon2lem1  25410  dfrdg2  25423  brbtwn2  25844  ax5seglem3  25870  ax5seglem6  25873  axpaschlem  25879  axcontlem2  25904  axcontlem4  25906  locfinbas  26381  cntotbnd  26505  heiborlem5  26524  heiborlem6  26525  psgnunilem5  27394  stoweidlem60  27785  cshwidxn  28247  cshweqrep  28274  cshwsame  28277  cshwssizelem4a  28283  bnj563  29111  bnj1212  29171  bnj1219  29172  bnj1366  29201  bnj1379  29202  bnj545  29266  bnj594  29283  bnj1118  29353  bnj1177  29375  bnj1190  29377  bnj1398  29403  bnj1417  29410  bnj1450  29419  bnj1312  29427  bnj1523  29440  atl0cl  30101  dalem-ccly  30482
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator