Theorem com34 83

Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)

Hypothesis

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

Assertion

Ref	Expression
com34	|- ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) )

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2		pm2.04 82	. 2 |- ( ( ch -> ( th -> ta ) ) -> ( th -> ( ch -> ta ) ) )
3	1, 2	syl6 33	1 |- ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com4l  84  com35  90  3an1rs  1222  rspct  2870  po2nr  4357  funssres  5314  f1ocnv2d  6152  tfrlem9  6407  nnmass  6575  nnmordi  6604  genpcdl  7634  genpcuu  7635  mulnqprl  7683  mulnqpru  7684  distrlem1prl  7697  distrlem1pru  7698  divgt0  8947  divge0  8948  uzind2  9487  facdiv  10885  dvdsabseq  12191  divgcdcoprm0  12456  lmodvsdi  14106