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

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
StepHypRef Expression
1 simplbi2com.1 . . 3
21simplbi2 625 . 2
32com12 31 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator