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

Theorem simp2bi 1021
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 197 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1018 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  smodm  7078  erdm  7381  ixpfn  7536  winafp  9121  inar1  9199  inatsk  9202  tskuni  9207  grur1  9244  supmullem1  10577  supmullem2  10578  supmul  10579  eluzelz  11168  elfz3nn0  11886  ico01fl0  12050  cshco  12918  swrds2  12999  ef01bndlem  14216  sin01bnd  14217  cos01bnd  14218  sin01gt0  14222  bitsss  14374  smueqlem  14438  gznegcl  14842  gzcjcl  14843  gzaddcl  14844  gzmulcl  14845  gzabssqcl  14848  4sqlem4a  14858  cshwshashlem2  15030  structcnvcnv  15095  structfun  15096  xpsff1o  15425  mre1cl  15451  drsbn0  16133  subgss  16769  symgfixelsi  17027  psgnunilem5  17086  pgpgrp  17181  slwsubg  17197  efgs1b  17321  efgsp1  17322  efgsres  17323  efgredeu  17337  efgred2  17338  efgcpbllemb  17340  srgmgp  17679  ringmgp  17721  irrednu  17868  lmodring  18034  lmodprop2d  18085  lssn0  18099  phlsrng  19129  ocvss  19164  obsss  19218  locfinbas  20468  fclsfil  20956  tmdtps  21022  tgptmd  21025  trgring  21116  tdrgdrng  21119  ngpms  21545  icopnfcnv  21866  xrhmeo  21870  oprpiece1res2  21876  phtpcer  21919  pcoval2  21940  pcoass  21948  clmsca  21989  cphsqrtcl  22055  bncms  22205  itg2ge0  22570  uc1pn0  22971  mon1pn0  22972  sinq12ge0  23328  cosq14gt0  23330  cosq14ge0  23331  sinord  23348  recosf1o  23349  resinf1o  23350  logrnaddcl  23389  logbcl  23569  relogbreexp  23577  atanf  23671  atanneg  23698  atancj  23701  efiatan  23703  atanlogaddlem  23704  atanlogadd  23705  atanlogsub  23707  efiatan2  23708  2efiatan  23709  tanatan  23710  dvatan  23726  areambl  23749  rlimcnp  23756  emgt0  23797  harmoniclbnd  23799  harmonicbnd4  23801  lgamgulmlem2  23820  2sqlem2  24155  2sqlem3  24157  dchrvmasumlem2  24199  dchrvmasumiflem1  24202  logdivbnd  24257  pntpbnd2  24288  pnt  24315  brbtwn2  24781  ax5seglem3  24807  ax5seglem6  24810  axpaschlem  24816  axcontlem2  24841  axcontlem4  24843  eengbas  24857  ebtwntg  24858  ecgrtg  24859  elntg  24860  clwwisshclwwlem  25379  subgores  25877  subgoid  25880  subgoinv  25881  subgoablo  25884  ghsubgolemOLD  25943  hst1a  27706  stge0  27712  sthil  27722  f1mptrn  28072  fsumrp0cl  28296  omndtos  28306  slmdsrg  28361  orngogrp  28403  psgnfzto1stlem  28452  elunitge0  28544  xrge0iifcnv  28578  xrge0iifcv  28579  xrge0iifiso  28580  rrextnlm  28646  rrextchr  28647  0elros  28831  0elsros  28838  voliune  28891  volfiniune  28892  bnj563  29341  bnj1212  29399  bnj1219  29400  bnj1366  29429  bnj1379  29430  bnj545  29494  bnj594  29511  bnj1118  29581  bnj1177  29603  bnj1190  29605  bnj1398  29631  bnj1417  29638  bnj1450  29647  bnj1312  29655  bnj1523  29668  msrval  29964  mclsppslem  30009  dfon2lem1  30216  dfrdg2  30229  cntotbnd  31832  heiborlem5  31851  heiborlem6  31852  atl0dm  32577  dalem-ccly  32959  stoweidlem60  37490  fourierdlem40  37578  fourierdlem78  37616  rngmgp  38636
  Copyright terms: Public domain W3C validator