Theorem com13 80

Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

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	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3r 79	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com23 78	1 |- ( ch -> ( ps -> ( ph -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com24  87  an13s  562  an31s  565  3imp31  1191  3imp21  1193  funopg  5232  f1o2ndf1  6207  brecop  6603  fiintim  6906  elpq  9607  xnn0lenn0nn0  9822  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  fzo1fzo0n0  10139  elfzodifsumelfzo  10157  ssfzo12  10180  ssfzo12bi  10181  facwordi  10674  fihashf1rn  10723  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  dfgcd2  11969  sqrt2irr  12116  zabsle1  13694  bj-inf2vnlem2  14006