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

Theorem an12s 779
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 775 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an12s.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
an12s  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  ->  th )

Proof of Theorem an12s
StepHypRef Expression
1 an12 775 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylbi 189 1  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360
This theorem is referenced by:  anabsan2  798  1stconst  6127  2ndconst  6128  oecl  6490  oaass  6513  odi  6531  oen0  6538  oeworde  6545  ltexprlem4  8617  uzind3OLD  10060  iccshftr  10721  iccshftl  10723  iccdil  10725  icccntr  10727  ndvdsadd  12555  eulerthlem2  12798  neips  16798  tx1stc  17292  filuni  17528  ufldom  17605  isch3  21767  unoplin  22446  hmoplin  22468  adjlnop  22612  chirredlem2  22917  btwnconn1lem12  24082  btwnconn1  24085  iscringd  25977  unichnidl  26009
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator