Theorem com3r 73

Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com3.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
com3r	|- ( ch -> ( ph -> ( ps -> th ) ) )

Proof of Theorem com3r

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com23 72	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
3	2	com12 27	1 |- ( ch -> ( ph -> ( ps -> 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:  com13  74  com3l  75  com14  82  expd  245  moexexdc  1984  euexex  1985  mob  2723  issref  4707  relresfld  4847  poxp  5853  nndi  6065  nnmass  6066  distrlem5prl  6684  distrlem5pru  6685  flqeqceilz  9160  ialgcvga  9890  ialgfx  9891