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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com24  87  an13s  539  an31s  542  funopg  5113  f1o2ndf1  6077  brecop  6471  fiintim  6768  xnn0lenn0nn0  9535  elfz0ubfz0  9789  elfz0fzfz0  9790  fz0fzelfz0  9791  fz0fzdiffz0  9794  fzo1fzo0n0  9847  elfzodifsumelfzo  9865  ssfzo12  9888  ssfzo12bi  9889  facwordi  10373  fihashf1rn  10422  oddnn02np1  11419  oddge22np1  11420  evennn02n  11421  evennn2n  11422  dfgcd2  11542  sqrt2irr  11680  bj-inf2vnlem2  12852