MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2bi 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  6580  abianfplem  6682  erdm  6882  ixpfn  7035  winafp  8536  inar1  8614  inatsk  8617  tskuni  8622  grur1  8659  supmullem1  9938  supmullem2  9939  supmul  9940  eluzelz  10460  elfz3nn0  11048  swrds2  11843  ef01bndlem  12748  sin01bnd  12749  cos01bnd  12750  sin01gt0  12754  bitsss  12901  smueqlem  12965  gznegcl  13266  gzcjcl  13267  gzaddcl  13268  gzmulcl  13269  gzabssqcl  13272  4sqlem4a  13282  structcnvcnv  13443  structfun  13444  xpsff1o  13756  mre1cl  13782  drsbn0  14357  subgss  14908  pgpgrp  15191  slwsubg  15207  efgs1b  15331  efgsp1  15332  efgsres  15333  efgredeu  15347  efgred2  15348  efgcpbllemb  15350  rngmgp  15633  irrednu  15773  lmodrng  15921  lmodprop2d  15969  lssn0  15980  phlsrng  16825  ocvss  16860  obsss  16914  fclsfil  18003  tmdtps  18067  tgptmd  18070  trgrng  18161  tdrgdrng  18164  ngpms  18608  icopnfcnv  18928  xrhmeo  18932  oprpiece1res2  18938  phtpcer  18981  pcoval2  19002  pcoass  19010  clmsca  19051  cphsqrcl  19108  bncms  19258  itg2ge0  19588  uc1pn0  20029  mon1pn0  20030  sinq12ge0  20377  cosq14gt0  20379  cosq14ge0  20380  sinord  20397  recosf1o  20398  resinf1o  20399  logrnaddcl  20433  atanf  20681  atanneg  20708  atancj  20711  efiatan  20713  atanlogaddlem  20714  atanlogadd  20715  atanlogsub  20717  efiatan2  20718  2efiatan  20719  tanatan  20720  dvatan  20736  areambl  20758  rlimcnp  20765  emgt0  20806  harmoniclbnd  20808  harmonicbnd4  20810  2sqlem2  21109  2sqlem3  21111  dchrvmasumlem2  21153  dchrvmasumiflem1  21156  logdivbnd  21211  pntpbnd2  21242  pnt  21269  subgores  21853  subgoid  21856  subgoinv  21857  subgoablo  21860  ghsubgolem  21919  hst1a  23682  stge0  23688  sthil  23698  fsumrp0cl  24178  ofldtos  24198  elunitge0  24258  xrge0iifcnv  24280  xrge0iifcv  24281  xrge0iifiso  24282  logbcl  24358  voliune  24546  volfiniune  24547  lgamgulmlem2  24775  dfon2lem1  25361  dfrdg2  25374  brbtwn2  25756  ax5seglem3  25782  ax5seglem6  25785  axpaschlem  25791  axcontlem2  25816  axcontlem4  25818  locfinbas  26279  cntotbnd  26403  heiborlem5  26422  heiborlem6  26423  psgnunilem5  27293  stoweidlem60  27684  bnj563  28829  bnj1212  28889  bnj1219  28890  bnj1366  28919  bnj1379  28920  bnj545  28984  bnj594  29001  bnj1118  29071  bnj1177  29093  bnj1190  29095  bnj1398  29121  bnj1417  29128  bnj1450  29137  bnj1312  29145  bnj1523  29158  atl0cl  29798  dalem-ccly  30179
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