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  1223  3imp21  1225  funopg  5391  f1o2ndf1  6437  brecop  6872  fiintim  7204  elpq  9999  xnn0lenn0nn0  10217  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  fzo1fzo0n0  10544  elfzodifsumelfzo  10568  ssfzo12  10591  ssfzo12bi  10592  facwordi  11127  fihashf1rn  11176  swrdswrdlem  11421  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem2  11448  swrdccat  11452  reuccatpfxs1lem  11463  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  dfgcd2  12735  sqrt2irr  12884  lmodfopnelem1  14598  mpomulcn  15557  zabsle1  15998  gausslemma2dlem1a  16057  2lgsoddprm  16112  upgredg2vtx  16269  usgruspgrben  16307  usgredg2vlem2  16344  edg0usgr  16368  uspgr2wlkeq  16486  clwwlkn1loopb  16541  clwwlkext2edg  16543  clwwlknonex2lem2  16559  bj-inf2vnlem2  16867