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  556  an31s  559  funopg  5157  f1o2ndf1  6125  brecop  6519  fiintim  6817  xnn0lenn0nn0  9648  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  fzo1fzo0n0  9960  elfzodifsumelfzo  9978  ssfzo12  10001  ssfzo12bi  10002  facwordi  10486  fihashf1rn  10535  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  dfgcd2  11702  sqrt2irr  11840  bj-inf2vnlem2  13169