Theorem an1s 544

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  1stconst 5070  2ndconst 5071  oecl 5218  oeclOLD 5219  oaass 5243  odi 5258  oen0 5261  oeordi 5262  oeworde 5268  unifi 5648  ac5b 5915  distrlem4pr 6282  prlem934b 6290  ltexprlem4 6297  uzind3OLD 7421  fsumrev 8289  climadd 8377  climmul 8388  caucvglem6 8422  fsum0diaglem2 8519  tgss2 8907  neiint 8995  neips 9003  minveclem9 9898  spansnmul 11120  unoplin 11481  hmoplin 11503  adjlnop 11656  irredlem2 11963  divalgmod 13709  ndvdsadd 13711  axfelem14 14044  fzdisj 15793  sdc 15811  iccshftr 15857  iccshftl 15859  iccdil 15861  icccntr 15863  txcnoprab 15911  sstotbnd 15936  heiborlem34 15988  unichnidl 16179

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 164  df-an 242

Copyright terms: Public domain