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  569  an31s  572  3imp31  1222  3imp21  1224  funopg  5360  f1o2ndf1  6392  brecop  6793  fiintim  7122  elpq  9882  xnn0lenn0nn0  10099  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  fzo1fzo0n0  10421  elfzodifsumelfzo  10445  ssfzo12  10468  ssfzo12bi  10469  facwordi  11001  fihashf1rn  11049  swrdswrdlem  11284  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  pfxccatin12lem2  11311  swrdccat  11315  reuccatpfxs1lem  11326  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  dfgcd2  12584  sqrt2irr  12733  lmodfopnelem1  14337  mpomulcn  15289  zabsle1  15727  gausslemma2dlem1a  15786  2lgsoddprm  15841  upgredg2vtx  15998  usgruspgrben  16036  usgredg2vlem2  16073  edg0usgr  16097  uspgr2wlkeq  16215  clwwlkn1loopb  16270  clwwlkext2edg  16272  clwwlknonex2lem2  16288  bj-inf2vnlem2  16566