MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an12s Structured version   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  6435  2ndconst  6436  oecl  6781  oaass  6804  odi  6822  oen0  6829  oeworde  6836  ltexprlem4  8916  uzind3OLD  10365  iccshftr  11030  iccshftl  11032  iccdil  11034  icccntr  11036  ndvdsadd  12928  eulerthlem2  13171  neips  17177  tx1stc  17682  filuni  17917  ufldom  17994  isch3  22744  unoplin  23423  hmoplin  23445  adjlnop  23589  chirredlem2  23894  btwnconn1lem12  26032  btwnconn1  26035  mblfinlem4  26246  iscringd  26609  unichnidl  26641
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