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  567  an31s  570  3imp31  1198  3imp21  1200  funopg  5293  f1o2ndf1  6295  brecop  6693  fiintim  7001  elpq  9742  xnn0lenn0nn0  9959  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  fzo1fzo0n0  10278  elfzodifsumelfzo  10296  ssfzo12  10319  ssfzo12bi  10320  facwordi  10851  fihashf1rn  10899  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  dfgcd2  12208  sqrt2irr  12357  lmodfopnelem1  13958  mpomulcn  14910  zabsle1  15348  gausslemma2dlem1a  15407  2lgsoddprm  15462  bj-inf2vnlem2  15725