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

Theorem an12s 776
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 772 is combined with syl 15 (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 772 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylbi 187 1  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anabsan2  795  1stconst  6223  2ndconst  6224  oecl  6552  oaass  6575  odi  6593  oen0  6600  oeworde  6607  ltexprlem4  8679  uzind3OLD  10123  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  ndvdsadd  12623  eulerthlem2  12866  neips  16866  tx1stc  17360  filuni  17596  ufldom  17673  isch3  21837  unoplin  22516  hmoplin  22538  adjlnop  22682  chirredlem2  22987  btwnconn1lem12  24793  btwnconn1  24796  iscringd  26727  unichnidl  26759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator