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  7081  erdm  7384  ixpfn  7539  winafp  9129  inar1  9207  inatsk  9210  tskuni  9215  grur1  9252  supmullem1  10584  supmullem2  10585  supmul  10586  eluzelz  11175  elfz3nn0  11895  ico01fl0  12059  cshco  12935  swrds2  13020  ef01bndlem  14237  sin01bnd  14238  cos01bnd  14239  sin01gt0  14243  bitsss  14398  smueqlem  14463  gznegcl  14878  gzcjcl  14879  gzaddcl  14880  gzmulcl  14881  gzabssqcl  14884  4sqlem4a  14894  cshwshashlem2  15066  structcnvcnv  15131  structfun  15132  xpsff1o  15473  mre1cl  15499  drsbn0  16181  subgss  16817  symgfixelsi  17075  psgnunilem5  17134  pgpgrp  17245  slwsubg  17261  efgs1b  17385  efgsp1  17386  efgsres  17387  efgredeu  17401  efgred2  17402  efgcpbllemb  17404  srgmgp  17743  ringmgp  17785  irrednu  17932  lmodring  18098  lmodprop2d  18149  lssn0  18163  phlsrng  19196  ocvss  19231  obsss  19285  locfinbas  20535  fclsfil  21023  tmdtps  21089  tgptmd  21092  trgring  21183  tdrgdrng  21186  ngpms  21612  icopnfcnv  21968  xrhmeo  21972  oprpiece1res2  21978  phtpcer  22024  pcoval2  22045  pcoass  22053  clmsca  22094  cphsqrtcl  22160  bncms  22310  itg2ge0  22691  uc1pn0  23094  mon1pn0  23095  sinq12ge0  23461  cosq14gt0  23463  cosq14ge0  23464  sinord  23481  recosf1o  23482  resinf1o  23483  logrnaddcl  23522  logbcl  23702  relogbreexp  23710  atanf  23804  atanneg  23831  atancj  23834  efiatan  23836  atanlogaddlem  23837  atanlogadd  23838  atanlogsub  23840  efiatan2  23841  2efiatan  23842  tanatan  23843  dvatan  23859  areambl  23882  rlimcnp  23889  emgt0  23930  harmoniclbnd  23932  harmonicbnd4  23934  lgamgulmlem2  23953  2sqlem2  24290  2sqlem3  24292  dchrvmasumlem2  24334  dchrvmasumiflem1  24337  logdivbnd  24392  pntpbnd2  24423  pnt  24450  brbtwn2  24933  ax5seglem3  24959  ax5seglem6  24962  axpaschlem  24968  axcontlem2  24993  axcontlem4  24995  eengbas  25009  ebtwntg  25010  ecgrtg  25011  elntg  25012  clwwisshclwwlem  25532  subgores  26030  subgoid  26033  subgoinv  26034  subgoablo  26037  ghsubgolemOLD  26096  hst1a  27869  stge0  27875  sthil  27885  f1mptrn  28234  fsumrp0cl  28465  omndtos  28475  slmdsrg  28530  orngogrp  28572  psgnfzto1stlem  28621  elunitge0  28713  xrge0iifcnv  28747  xrge0iifcv  28748  xrge0iifiso  28749  rrextnlm  28815  rrextchr  28816  0elros  29000  0elsros  29007  voliune  29060  volfiniune  29061  bnj563  29561  bnj1212  29619  bnj1219  29620  bnj1366  29649  bnj1379  29650  bnj545  29714  bnj594  29731  bnj1118  29801  bnj1177  29823  bnj1190  29825  bnj1398  29851  bnj1417  29858  bnj1450  29867  bnj1312  29875  bnj1523  29888  msrval  30184  mclsppslem  30229  dfon2lem1  30436  dfrdg2  30449  cntotbnd  32092  heiborlem5  32111  heiborlem6  32112  atl0dm  32837  dalem-ccly  33219  stoweidlem60  37861  fourierdlem40  37950  fourierdlem78  37988  rngmgp  39498
  Copyright terms: Public domain W3C validator