Theorem an1rs 373

Description: Deduction rearranging conjuncts.

Hypothesis

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

Assertion

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

Proof of Theorem an1rs

Step	Hyp	Ref	Expression
1		an23 371	. 2 |- (((ph /\ ch) /\ ps) <-> ((ph /\ ps) /\ ch))
2		an1rs.1	. 2 |- (((ph /\ ps) /\ ch) -> th)
3	1, 2	sylbi 174	1 |- (((ph /\ ch) /\ ps) -> th)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anabsan 386  ordunisssuc 2334  fssres 2764  f1ores 2813  fconstfv 2903  f1oiso 2942  oaordi 3148  oaass 3163  undom 3342  mapenlem1 3384  mapenlem2 3385  mapxpen 3390  mapunen 3397  isfinite2 3437  suplem1pr 3955  suplem2pr 3956  recexsrlem 4006  suppsr2 4017  divdivdivt 4265  uzind 4603  qrecclt 4646  infxpidmlem10 4942  infdif 4948  infxpabs 4949  infmap1 4950  ocsh 5164  occllem6 5185  projlem25 5217  projlem26 5218  shscl 5282  mdbr2 5728  atcvatlem 5770

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org