Theorem com13 33

Description: Commutation of antecedents. Swap 1st and 3rd.

Hypothesis

Ref	Expression
com3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
com13	|- (ch -> (ps -> (ph -> th)))

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . . 4 |- (ph -> (ps -> (ch -> th)))
2	1	com12 13	. . 3 |- (ps -> (ph -> (ch -> th)))
3	2	com23 32	. 2 |- (ps -> (ch -> (ph -> th)))
4	3	com12 13	1 |- (ch -> (ps -> (ph -> th)))

Syntax hints:   -> wi 2

This theorem is referenced by:  com3l 34  com14 38  peano5 2394  isomin 2937  tfrlem8 2956  tfrlem9 2957  abianfp 3000  omordi 3164  brecop 3242  isfinite2 3437  fiint 3445  aceq5 3563  aceq6b 3565  carduni 3664  mulgt0sr 4008  infxpidmlem7 4939  infxpidmlem12 4944  projlem15 5207  projlem26 5218  shmods 5363  mdsymlem6 5781  mdsymlem7 5782

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

metamath.org