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

Theorem simp2bi 1010
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 194 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 1007 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  smodm  7014  erdm  7313  ixpfn  7468  winafp  9064  inar1  9142  inatsk  9145  tskuni  9150  grur1  9187  supmullem1  10504  supmullem2  10505  supmul  10506  eluzelz  11091  elfz3nn0  11776  ico01fl0  11935  cshco  12793  swrds2  12874  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  sin01gt0  14007  bitsss  14160  smueqlem  14224  gznegcl  14537  gzcjcl  14538  gzaddcl  14539  gzmulcl  14540  gzabssqcl  14543  4sqlem4a  14553  cshwshashlem2  14665  structcnvcnv  14727  structfun  14728  xpsff1o  15057  mre1cl  15083  drsbn0  15765  subgss  16401  symgfixelsi  16659  psgnunilem5  16718  pgpgrp  16813  slwsubg  16829  efgs1b  16953  efgsp1  16954  efgsres  16955  efgredeu  16969  efgred2  16970  efgcpbllemb  16972  srgmgp  17357  ringmgp  17399  irrednu  17549  lmodring  17715  lmodprop2d  17767  lssn0  17782  phlsrng  18839  ocvss  18874  obsss  18928  locfinbas  20189  fclsfil  20677  tmdtps  20741  tgptmd  20744  trgring  20839  tdrgdrng  20842  ngpms  21286  icopnfcnv  21608  xrhmeo  21612  oprpiece1res2  21618  phtpcer  21661  pcoval2  21682  pcoass  21690  clmsca  21731  cphsqrtcl  21797  bncms  21949  itg2ge0  22308  uc1pn0  22712  mon1pn0  22713  sinq12ge0  23067  cosq14gt0  23069  cosq14ge0  23070  sinord  23087  recosf1o  23088  resinf1o  23089  logrnaddcl  23128  logbcl  23306  relogbreexp  23314  atanf  23408  atanneg  23435  atancj  23438  efiatan  23440  atanlogaddlem  23441  atanlogadd  23442  atanlogsub  23444  efiatan2  23445  2efiatan  23446  tanatan  23447  dvatan  23463  areambl  23486  rlimcnp  23493  emgt0  23534  harmoniclbnd  23536  harmonicbnd4  23538  2sqlem2  23837  2sqlem3  23839  dchrvmasumlem2  23881  dchrvmasumiflem1  23884  logdivbnd  23939  pntpbnd2  23970  pnt  23997  brbtwn2  24410  ax5seglem3  24436  ax5seglem6  24439  axpaschlem  24445  axcontlem2  24470  axcontlem4  24472  eengbas  24486  ebtwntg  24487  ecgrtg  24488  elntg  24489  clwwisshclwwlem  25008  subgores  25504  subgoid  25507  subgoinv  25508  subgoablo  25511  ghsubgolemOLD  25570  hst1a  27335  stge0  27341  sthil  27351  f1mptrn  27693  fsumrp0cl  27919  omndtos  27929  slmdsrg  27984  orngogrp  28026  elunitge0  28116  xrge0iifcnv  28150  xrge0iifcv  28151  xrge0iifiso  28152  rrextnlm  28218  rrextchr  28219  voliune  28438  volfiniune  28439  lgamgulmlem2  28836  msrval  29162  mclsppslem  29207  dfon2lem1  29455  dfrdg2  29468  cntotbnd  30532  heiborlem5  30551  heiborlem6  30552  stoweidlem60  32081  fourierdlem40  32168  fourierdlem78  32206  rngmgp  32938  bnj563  34201  bnj1212  34259  bnj1219  34260  bnj1366  34289  bnj1379  34290  bnj545  34354  bnj594  34371  bnj1118  34441  bnj1177  34463  bnj1190  34465  bnj1398  34491  bnj1417  34498  bnj1450  34507  bnj1312  34515  bnj1523  34528  atl0dm  35424  dalem-ccly  35806
  Copyright terms: Public domain W3C validator