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  6207  2ndconst  6208  oecl  6536  oaass  6559  odi  6577  oen0  6584  oeworde  6591  ltexprlem4  8663  uzind3OLD  10107  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  ndvdsadd  12607  eulerthlem2  12850  neips  16850  tx1stc  17344  filuni  17580  ufldom  17657  isch3  21821  unoplin  22500  hmoplin  22522  adjlnop  22666  chirredlem2  22971  btwnconn1lem12  24721  btwnconn1  24724  iscringd  26624  unichnidl  26656
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