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  557  an31s  560  3imp31  1186  3imp21  1188  funopg  5222  f1o2ndf1  6196  brecop  6591  fiintim  6894  elpq  9586  xnn0lenn0nn0  9801  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  fz0fzdiffz0  10065  fzo1fzo0n0  10118  elfzodifsumelfzo  10136  ssfzo12  10159  ssfzo12bi  10160  facwordi  10653  fihashf1rn  10702  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  dfgcd2  11947  sqrt2irr  12094  zabsle1  13540  bj-inf2vnlem2  13853