Theorem an1s 485

Description: Deduction rearranging conjuncts.

Hypothesis

Ref	Expression
an1s.1	|- ((ph /\ (ps /\ ch)) -> th)

Assertion

Ref	Expression
an1s	|- ((ps /\ (ph /\ ch)) -> th)

Proof of Theorem an1s

Step	Hyp	Ref	Expression
1		an12 483	. 2 |- ((ps /\ (ph /\ ch)) <-> (ph /\ (ps /\ ch)))
2		an1s.1	. 2 |- ((ph /\ (ps /\ ch)) -> th)
3	1, 2	sylbi 199	1 |- ((ps /\ (ph /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oecl 4156  oaass 4179  odi 4194  oen0 4197  oeordi 4198  oeworde 4204  unifi 4532  ac5b 4725  distrlem4pr 5102  prlem934b 5110  ltexprlem4 5117  uzind3OLD 6157  fsumrev 6967  climadd 7053  climmul 7064  caucvglem6 7098  fsum0diaglem2 7192  tgss2t 7579  neiint 7660  neips 7668  minveclem9 8484  spansnmul 9403  unoplint 9760  hmoplint 9782  adjlnopt 9934  irredlem2 10226

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain