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

Theorem an12s 801
 Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 797 is combined with syl 16 (or a variant). (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an12s.1
Assertion
Ref Expression
an12s

Proof of Theorem an12s
StepHypRef Expression
1 an12 797 . 2
2 an12s.1 . 2
31, 2sylbi 195 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  anabsan2  822  1stconst  6888  2ndconst  6889  oecl  7206  oaass  7229  odi  7247  oen0  7254  oeworde  7261  ltexprlem4  9438  uzind3OLD  10983  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  ndvdsadd  14066  eulerthlem2  14312  neips  19614  tx1stc  20151  filuni  20386  ufldom  20463  isch3  26159  unoplin  26839  hmoplin  26861  adjlnop  27005  chirredlem2  27310  btwnconn1lem12  29748  btwnconn1  29751  mblfinlem4  30054  iscringd  30396  unichnidl  30428 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