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  6059  2ndconst  6060  oecl  6422  oaass  6445  odi  6463  oen0  6470  oeworde  6477  ltexprlem4  8543  uzind3OLD  9986  iccshftr  10647  iccshftl  10649  iccdil  10651  icccntr  10653  ndvdsadd  12481  eulerthlem2  12724  neips  16682  tx1stc  17176  filuni  17412  ufldom  17489  isch3  21651  unoplin  22330  hmoplin  22352  adjlnop  22496  chirredlem2  22801  btwnconn1lem12  23895  btwnconn1  23898  iscringd  25790  unichnidl  25822
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