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  1243  rspct  2900  po2nr  4400  funssres  5360  f1ocnv2d  6210  tfrlem9  6465  nnmass  6633  nnmordi  6662  genpcdl  7706  genpcuu  7707  mulnqprl  7755  mulnqpru  7756  distrlem1prl  7769  distrlem1pru  7770  divgt0  9019  divge0  9020  uzind2  9559  facdiv  10960  swrdswrdlem  11236  wrd2ind  11255  dvdsabseq  12358  divgcdcoprm0  12623  lmodvsdi  14275