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  5411  f1o2ndf1  6464  brecop  6899  fiintim  7238  elpq  10059  xnn0lenn0nn0  10277  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  fzo1fzo0n0  10605  elfzodifsumelfzo  10629  ssfzo12  10652  ssfzo12bi  10653  facwordi  11192  fihashf1rn  11241  swrdswrdlem  11490  swrdswrd  11491  wrd2ind  11509  swrdccatin1  11511  pfxccatin12lem2  11517  swrdccat  11521  reuccatpfxs1lem  11532  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  dfgcd2  12807  sqrt2irr  12957  lmodfopnelem1  14710  mpomulcn  15716  zabsle1  16216  gausslemma2dlem1a  16275  2lgsoddprm  16330  upgredg2vtx  16487  usgruspgrben  16525  usgredg2vlem2  16562  edg0usgr  16586  uspgr2wlkeq  16704  clwwlkn1loopb  16759  clwwlkext2edg  16761  clwwlknonex2lem2  16777  bj-inf2vnlem2  17095