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

Theorem simp2bi 1030
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 199 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1027 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  smodm  7101  erdm  7404  ixpfn  7559  winafp  9153  inar1  9231  inatsk  9234  tskuni  9239  grur1  9276  supmullem1  10610  supmullem2  10611  supmul  10612  eluzelz  11202  elfz3nn0  11923  ico01fl0  12091  cshco  12976  swrds2  13072  ef01bndlem  14293  sin01bnd  14294  cos01bnd  14295  sin01gt0  14299  bitsss  14454  smueqlem  14519  gznegcl  14934  gzcjcl  14935  gzaddcl  14936  gzmulcl  14937  gzabssqcl  14940  4sqlem4a  14950  cshwshashlem2  15122  structcnvcnv  15187  structfun  15188  xpsff1o  15529  mre1cl  15555  drsbn0  16237  subgss  16873  symgfixelsi  17131  psgnunilem5  17190  pgpgrp  17301  slwsubg  17317  efgs1b  17441  efgsp1  17442  efgsres  17443  efgredeu  17457  efgred2  17458  efgcpbllemb  17460  srgmgp  17799  ringmgp  17841  irrednu  17988  lmodring  18154  lmodprop2d  18205  lssn0  18219  phlsrng  19253  ocvss  19288  obsss  19342  locfinbas  20592  fclsfil  21080  tmdtps  21146  tgptmd  21149  trgring  21240  tdrgdrng  21243  ngpms  21669  icopnfcnv  22025  xrhmeo  22029  oprpiece1res2  22035  phtpcer  22081  pcoval2  22102  pcoass  22110  clmsca  22151  cphsqrtcl  22217  bncms  22367  itg2ge0  22749  uc1pn0  23152  mon1pn0  23153  sinq12ge0  23519  cosq14gt0  23521  cosq14ge0  23522  sinord  23539  recosf1o  23540  resinf1o  23541  logrnaddcl  23580  logbcl  23760  relogbreexp  23768  atanf  23862  atanneg  23889  atancj  23892  efiatan  23894  atanlogaddlem  23895  atanlogadd  23896  atanlogsub  23898  efiatan2  23899  2efiatan  23900  tanatan  23901  dvatan  23917  areambl  23940  rlimcnp  23947  emgt0  23988  harmoniclbnd  23990  harmonicbnd4  23992  lgamgulmlem2  24011  2sqlem2  24348  2sqlem3  24350  dchrvmasumlem2  24392  dchrvmasumiflem1  24395  logdivbnd  24450  pntpbnd2  24481  pnt  24508  brbtwn2  24991  ax5seglem3  25017  ax5seglem6  25020  axpaschlem  25026  axcontlem2  25051  axcontlem4  25053  eengbas  25067  ebtwntg  25068  ecgrtg  25069  elntg  25070  clwwisshclwwlem  25590  subgores  26088  subgoid  26091  subgoinv  26092  subgoablo  26095  ghsubgolemOLD  26154  hst1a  27927  stge0  27933  sthil  27943  f1mptrn  28285  fsumrp0cl  28509  omndtos  28519  slmdsrg  28574  orngogrp  28615  psgnfzto1stlem  28664  elunitge0  28756  xrge0iifcnv  28790  xrge0iifcv  28791  xrge0iifiso  28792  rrextnlm  28858  rrextchr  28859  0elros  29043  0elsros  29050  voliune  29102  volfiniune  29103  bnj563  29603  bnj1212  29661  bnj1219  29662  bnj1366  29691  bnj1379  29692  bnj545  29756  bnj594  29773  bnj1118  29843  bnj1177  29865  bnj1190  29867  bnj1398  29893  bnj1417  29900  bnj1450  29909  bnj1312  29917  bnj1523  29930  msrval  30226  mclsppslem  30271  dfon2lem1  30479  dfrdg2  30492  cntotbnd  32174  heiborlem5  32193  heiborlem6  32194  atl0dm  32914  dalem-ccly  33296  stoweidlem60  38022  fourierdlem40  38111  fourierdlem78  38149  elfzo0l  39206  rngmgp  40247
  Copyright terms: Public domain W3C validator