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  1199  3imp21  1201  funopg  5306  f1o2ndf1  6316  brecop  6714  fiintim  7030  elpq  9772  xnn0lenn0nn0  9989  elfz0ubfz0  10249  elfz0fzfz0  10250  fz0fzelfz0  10251  fz0fzdiffz0  10254  fzo1fzo0n0  10309  elfzodifsumelfzo  10332  ssfzo12  10355  ssfzo12bi  10356  facwordi  10887  fihashf1rn  10935  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  dfgcd2  12368  sqrt2irr  12517  lmodfopnelem1  14119  mpomulcn  15071  zabsle1  15509  gausslemma2dlem1a  15568  2lgsoddprm  15623  bj-inf2vnlem2  15944