Theorem an1s 486

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 484	. 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 4172  oaass 4195  odi 4210  oen0 4213  oeordi 4214  oeworde 4220  unifiOLD 4557  ac5b 4753  distrlem4pr 5130  prlem934b 5138  ltexprlem4 5145  uzind3OLD 6209  intfracqOLD 6255  fsumrev 7029  climadd 7117  climmul 7128  caucvglem6 7162  fsum0diaglem2 7257  tgss2t 7637  neiint 7719  neips 7727  minveclem9 8553  spansnmul 9487  unoplint 9844  hmoplint 9866  adjlnopt 10019  irredlem2 10318

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