Theorem an1s 497

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 495	. 2 |- ((ps /\ (ph /\ ch)) <-> (ph /\ (ps /\ ch)))
2		an1s.1	. 2 |- ((ph /\ (ps /\ ch)) -> th)
3	1, 2	sylbi 206	1 |- ((ps /\ (ph /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  oecl 4230  oaass 4253  odi 4268  oen0 4271  oeordi 4272  oeworde 4278  unifi 4618  ac5b 4815  distrlem4pr 5195  prlem934b 5203  ltexprlem4 5210  uzind3OLD 6294  fsumrev 7119  climadd 7207  climmul 7218  caucvglem6 7252  fsum0diaglem2 7347  tgss2 7726  neiint 7804  neips 7812  minveclem9 8637  spansnmul 9570  unoplin 9927  hmoplin 9949  adjlnop 10102  irredlem2 10402

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 154  df-an 232

Copyright terms: Public domain