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

Theorem an12s 778
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 774 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 774 . 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  797  1stconst  6168  2ndconst  6169  oecl  6531  oaass  6554  odi  6572  oen0  6579  oeworde  6586  ltexprlem4  8658  uzind3OLD  10102  iccshftr  10763  iccshftl  10765  iccdil  10767  icccntr  10769  ndvdsadd  12601  eulerthlem2  12844  neips  16844  tx1stc  17338  filuni  17574  ufldom  17651  isch3  21813  unoplin  22492  hmoplin  22514  adjlnop  22658  chirredlem2  22963  btwnconn1lem12  24128  btwnconn1  24131  iscringd  26023  unichnidl  26055
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