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  6106  2ndconst  6107  oecl  6469  oaass  6492  odi  6510  oen0  6517  oeworde  6524  ltexprlem4  8596  uzind3OLD  10039  iccshftr  10700  iccshftl  10702  iccdil  10704  icccntr  10706  ndvdsadd  12534  eulerthlem2  12777  neips  16777  tx1stc  17271  filuni  17507  ufldom  17584  isch3  21746  unoplin  22425  hmoplin  22447  adjlnop  22591  chirredlem2  22896  btwnconn1lem12  24061  btwnconn1  24064  iscringd  25956  unichnidl  25988
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