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  5305  f1o2ndf1  6314  brecop  6712  fiintim  7028  elpq  9770  xnn0lenn0nn0  9987  elfz0ubfz0  10247  elfz0fzfz0  10248  fz0fzelfz0  10249  fz0fzdiffz0  10252  fzo1fzo0n0  10307  elfzodifsumelfzo  10330  ssfzo12  10353  ssfzo12bi  10354  facwordi  10885  fihashf1rn  10933  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  dfgcd2  12335  sqrt2irr  12484  lmodfopnelem1  14086  mpomulcn  15038  zabsle1  15476  gausslemma2dlem1a  15535  2lgsoddprm  15590  bj-inf2vnlem2  15907