Theorem com13 79

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 78	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com23 77	1 |- ( ch -> ( ps -> ( ph -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com24  86  an13s  531  an31s  534  funopg  4954  f1o2ndf1  5869  brecop  6219  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  fzo1fzo0n0  9192  elfzodifsumelfzo  9210  ssfzo12  9233  ssfzo12bi  9234  facwordi  9667  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  dfgcd2  10403  sqrt2irr  10541  bj-inf2vnlem2  10766