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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  87  an13s  573  an31s  576  3imp31  1227  3imp21  1229  funopg  5414  f1o2ndf1  6468  brecop  6903  fiintim  7242  elpq  10066  xnn0lenn0nn0  10284  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  fzo1fzo0n0  10612  elfzodifsumelfzo  10636  ssfzo12  10659  ssfzo12bi  10660  facwordi  11200  fihashf1rn  11249  swrdswrdlem  11498  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem2  11525  swrdccat  11529  reuccatpfxs1lem  11540  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  dfgcd2  12816  sqrt2irr  12966  lmodfopnelem1  14770  mpomulcn  15792  zabsle1  16323  gausslemma2dlem1a  16382  2lgsoddprm  16437  upgredg2vtx  16594  usgruspgrben  16632  usgredg2vlem2  16669  edg0usgr  16693  uspgr2wlkeq  16811  clwwlkn1loopb  16866  clwwlkext2edg  16868  clwwlknonex2lem2  16884  bj-inf2vnlem2  17202