Theorem simplbi2com 627

Description: A deduction eliminating a conjunct, similar to simplbi2 625. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)

Hypothesis

Ref	Expression
simplbi2com.1

Assertion

Ref	Expression
simplbi2com

Proof of Theorem simplbi2com

Step	Hyp	Ref	Expression
1		simplbi2com.1	. . 3
2	1	simplbi2 625	. 2
3	2	com12 31	1

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

This theorem is referenced by:  mo2OLD  2334  elres  5314  xpidtr  5394  elovmpt2rab  6521  elovmpt2rab1  6522  inficl  7905  cfslb2n  8669  repswcshw  12780  cshw1  12790  bezoutlem1  14176  bezoutlem3  14178  modprmn0modprm0  14332  cnprest  19790  haust1  19853  lly1stc  19997  3cyclfrgrarn1  25012  dfon2lem9  29223  funcoressn  32212  ndmaovdistr  32292  2elfz3nn0  32332  sb5ALT  33295  onfrALTlem2  33318  onfrALTlem2VD  33689  sb5ALTVD  33713

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