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  6380  brecop  6780  fiintim  7104  elpq  9856  xnn0lenn0nn0  10073  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  fzo1fzo0n0  10395  elfzodifsumelfzo  10419  ssfzo12  10442  ssfzo12bi  10443  facwordi  10974  fihashf1rn  11022  swrdswrdlem  11252  swrdswrd  11253  wrd2ind  11271  swrdccatin1  11273  pfxccatin12lem2  11279  swrdccat  11283  reuccatpfxs1lem  11294  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  dfgcd2  12551  sqrt2irr  12700  lmodfopnelem1  14304  mpomulcn  15256  zabsle1  15694  gausslemma2dlem1a  15753  2lgsoddprm  15808  upgredg2vtx  15962  usgruspgrben  16000  usgredg2vlem2  16037  uspgr2wlkeq  16111  clwwlkn1loopb  16162  clwwlkext2edg  16164  bj-inf2vnlem2  16417