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

Theorem simplbi2com 631
 Description: A deduction eliminating a conjunct, similar to simplbi2 629. (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 629 . 2
32com12 32 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370 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 188  df-an 372 This theorem is referenced by:  elres  5102  xpidtr  5184  elovmpt2rab  6473  elovmpt2rab1  6474  inficl  7892  cfslb2n  8649  repswcshw  12857  cshw1  12867  bezoutlem1  14446  bezoutlem3OLD  14448  bezoutlem3  14451  modprmn0modprm0  14701  cnprest  20247  haust1  20310  lly1stc  20453  3cyclfrgrarn1  25682  dfon2lem9  30388  phpreu  31836  poimirlem26  31873  sb5ALT  36795  onfrALTlem2  36825  onfrALTlem2VD  37202  sb5ALTVD  37226  funcoressn  38442  ndmaovdistr  38522  reuccatpfxs1  38788  2elfz3nn0  38853
 Copyright terms: Public domain W3C validator