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  5324  f1o2ndf1  6337  brecop  6735  fiintim  7054  elpq  9805  xnn0lenn0nn0  10022  elfz0ubfz0  10282  elfz0fzfz0  10283  fz0fzelfz0  10284  fz0fzdiffz0  10287  fzo1fzo0n0  10344  elfzodifsumelfzo  10367  ssfzo12  10390  ssfzo12bi  10391  facwordi  10922  fihashf1rn  10970  swrdswrdlem  11195  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  pfxccatin12lem2  11222  swrdccat  11226  reuccatpfxs1lem  11237  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  dfgcd2  12450  sqrt2irr  12599  lmodfopnelem1  14201  mpomulcn  15153  zabsle1  15591  gausslemma2dlem1a  15650  2lgsoddprm  15705  upgredg2vtx  15852  bj-inf2vnlem2  16106