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  1221  rspct  2858  po2nr  4341  funssres  5297  f1ocnv2d  6124  tfrlem9  6374  nnmass  6542  nnmordi  6571  genpcdl  7581  genpcuu  7582  mulnqprl  7630  mulnqpru  7631  distrlem1prl  7644  distrlem1pru  7645  divgt0  8893  divge0  8894  uzind2  9432  facdiv  10812  dvdsabseq  11992  divgcdcoprm0  12242  lmodvsdi  13810