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

Theorem simp2bi 971
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 186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 968 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  smodm  6368  abianfplem  6470  erdm  6670  ixpfn  6822  winafp  8319  inar1  8397  inatsk  8400  tskuni  8405  grur1  8442  supmullem1  9720  supmullem2  9721  supmul  9722  eluzelz  10238  elfz3nn0  10823  swrds2  11560  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  bitsss  12617  smueqlem  12681  gznegcl  12982  gzcjcl  12983  gzaddcl  12984  gzmulcl  12985  gzabssqcl  12988  4sqlem4a  12998  structcnvcnv  13159  structfun  13160  xpsff1o  13470  mre1cl  13496  drsbn0  14071  subgss  14622  pgpgrp  14905  slwsubg  14921  efgs1b  15045  efgsp1  15046  efgsres  15047  efgredeu  15061  efgred2  15062  efgcpbllemb  15064  rngmgp  15347  irrednu  15487  lmodrng  15635  lmodprop2d  15687  lssn0  15698  phlsrng  16535  ocvss  16570  obsss  16624  fclsfil  17705  tmdtps  17759  tgptmd  17762  trgrng  17853  tdrgdrng  17856  ngpms  18122  icopnfcnv  18440  xrhmeo  18444  oprpiece1res2  18450  phtpcer  18493  pcoval2  18514  pcoass  18522  clmsca  18563  cphsqrcl  18620  bncms  18766  itg2ge0  19090  uc1pn0  19531  mon1pn0  19532  sinq12ge0  19876  cosq14gt0  19878  cosq14ge0  19879  sinord  19896  recosf1o  19897  resinf1o  19898  logrnaddcl  19931  atanf  20176  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  dvatan  20231  areambl  20253  rlimcnp  20260  emgt0  20300  harmoniclbnd  20302  harmonicbnd4  20304  2sqlem2  20603  2sqlem3  20605  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  logdivbnd  20705  pntpbnd2  20736  pnt  20763  subgores  20971  subgoid  20974  subgoinv  20975  subgoablo  20978  ghsubgolem  21037  hst1a  22798  stge0  22804  sthil  22814  elunitge0  23283  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifiso  23317  fsumrp0cl  23334  dfon2lem1  24139  dfrdg2  24152  brbtwn2  24533  ax5seglem3  24559  ax5seglem6  24562  axpaschlem  24568  axcontlem2  24593  axcontlem4  24595  locfinbas  26301  cntotbnd  26520  heiborlem5  26539  heiborlem6  26540  psgnunilem5  27417  stoweidlem60  27809  bnj563  28772  bnj1212  28832  bnj1219  28833  bnj1366  28862  bnj1379  28863  bnj545  28927  bnj594  28944  bnj1118  29014  bnj1177  29036  bnj1190  29038  bnj1398  29064  bnj1417  29071  bnj1450  29080  bnj1312  29088  bnj1523  29101  atl0cl  29493  dalem-ccly  29874
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator