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

Theorem an12s 777
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 773 is combined with syl 16 (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 773 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12s.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylbi 188 1  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anabsan2  796  1stconst  6394  2ndconst  6395  oecl  6740  oaass  6763  odi  6781  oen0  6788  oeworde  6795  ltexprlem4  8872  uzind3OLD  10321  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  ndvdsadd  12883  eulerthlem2  13126  neips  17132  tx1stc  17635  filuni  17870  ufldom  17947  isch3  22697  unoplin  23376  hmoplin  23398  adjlnop  23542  chirredlem2  23847  btwnconn1lem12  25936  btwnconn1  25939  mblfinlem3  26145  iscringd  26499  unichnidl  26531
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 178  df-an 361
  Copyright terms: Public domain W3C validator