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  1220  3imp21  1222  funopg  5352  f1o2ndf1  6374  brecop  6772  fiintim  7093  elpq  9844  xnn0lenn0nn0  10061  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  fzo1fzo0n0  10383  elfzodifsumelfzo  10407  ssfzo12  10430  ssfzo12bi  10431  facwordi  10962  fihashf1rn  11010  swrdswrdlem  11236  swrdswrd  11237  wrd2ind  11255  swrdccatin1  11257  pfxccatin12lem2  11263  swrdccat  11267  reuccatpfxs1lem  11278  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  dfgcd2  12535  sqrt2irr  12684  lmodfopnelem1  14288  mpomulcn  15240  zabsle1  15678  gausslemma2dlem1a  15737  2lgsoddprm  15792  upgredg2vtx  15946  usgruspgrben  15984  usgredg2vlem2  16021  uspgr2wlkeq  16076  bj-inf2vnlem2  16334