Theorem simplbi2 625

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
simplbi2.1

Assertion

Ref	Expression
simplbi2

Proof of Theorem simplbi2

Step	Hyp	Ref	Expression
1		simplbi2.1	. . 3
2	1	biimpri 206	. 2
3	2	ex 434	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  simplbi2com  627  sspss  3602  neldif  3628  reuss2  3777  pssdifn0  3888  ordunidif  4931  eceqoveq  7435  infxpenlem  8412  ackbij1lem18  8638  isf32lem2  8755  ingru  9214  indpi  9306  nqereu  9328  elfz0ubfz0  11807  elfzmlbp  11815  fzo1fzo0n0  11864  elfzo0z  11865  fzofzim  11869  elfzodifsumelfzo  11882  ccatval1lsw  12602  2swrd1eqwrdeq  12679  swrdswrd  12685  swrdccatin1  12708  swrd2lsw  12890  algcvga  14208  pcprendvds  14364  restntr  19683  filcon  20384  filssufilg  20412  ufileu  20420  ufilen  20431  alexsubALTlem3  20549  blcld  21008  causs  21737  itg2addlem  22165  rplogsum  23712  sizeusglecusglem1  24484  clwlkisclwwlklem1  24787  clwwlknwwlkncl  24800  numclwwlk2lem1  25102  ofpreima2  27508  esumpinfval  28079  eulerpartlemf  28309  sltres  29424  fin2so  30040  fdc  30238  ndmaovass  32291  elfz2z  32331  usgra2pth  32354  onfrALTlem2  33318  3ornot23VD  33647  ordelordALTVD  33667  onfrALTlem2VD  33689  bj-elid2  34600  lshpcmp  34713  lfl1  34795

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 371