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

Theorem simplbi2 612
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 31160. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
pm3.26bi2.1
Assertion
Ref Expression
simplbi2

Proof of Theorem simplbi2
StepHypRef Expression
1 pm3.26bi2.1 . . 3
21biimpri 200 . 2
32ex 427 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362
This theorem is referenced by:  simplbi2com  1409  sspss  3432  neldif  3458  reuss2  3607  pssdifn0  3717  ordunidif  4738  eceqoveq  7166  infxpenlem  8127  ackbij1lem18  8353  isf32lem2  8470  ingru  8928  indpi  9022  nqereu  9044  elfzelfzelfz  11428  elfzmlbp  11435  fzo1fzo0n0  11529  elfzo0z  11530  fzofzim  11534  elfzodifsumelfzo  11545  ccatval1lsw  12224  2swrd1eqwrdeq  12289  swrdswrd  12295  swrdccatin1  12315  swrd2lsw  12493  algcvga  13694  pcprendvds  13847  restntr  18490  filcon  19160  filssufilg  19188  ufileu  19196  ufilen  19207  alexsubALTlem3  19325  blcld  19780  causs  20509  itg2addlem  20936  rplogsum  22517  sizeusglecusglem1  23071  esumpinfval  26231  eulerpartlemf  26456  sltres  27507  fin2so  28087  fdc  28312  ndmaovass  29786  elfz2z  29872  ccats1rev  29934  usgra2pth  29975  clwlkisclwwlklem1  30123  clwwlknwwlkncl  30136  numclwwlk2lem1  30369  onfrALTlem2  30831  3ornot23VD  31161  ordelordALTVD  31181  onfrALTlem2VD  31203  lshpcmp  32070  lfl1  32152
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 179  df-an 364
  Copyright terms: Public domain W3C validator