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

Step	Hyp	Ref	Expression
1		pm3.26bi2.1	. . 3
2	1	biimpri 200	. 2
3	2	ex 427	1

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