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  2861  po2nr  4345  funssres  5301  f1ocnv2d  6131  tfrlem9  6386  nnmass  6554  nnmordi  6583  genpcdl  7603  genpcuu  7604  mulnqprl  7652  mulnqpru  7653  distrlem1prl  7666  distrlem1pru  7667  divgt0  8916  divge0  8917  uzind2  9455  facdiv  10847  dvdsabseq  12029  divgcdcoprm0  12294  lmodvsdi  13943