Theorem com34 82

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 81	. 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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com4l  83  com35  89  3an1rs  1150  rspct  2694  po2nr  4064  funssres  4962  f1ocnv2d  5724  tfrlem9  5958  nnmass  6089  nnmordi  6112  genpcdl  6709  genpcuu  6710  mulnqprl  6758  mulnqpru  6759  distrlem1prl  6772  distrlem1pru  6773  divgt0  7950  divge0  7951  uzind2  8459  facdiv  9665  dvdsabseq  10247  divgcdcoprm0  10483