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  1219  rspct  2836  po2nr  4311  funssres  5260  f1ocnv2d  6077  tfrlem9  6322  nnmass  6490  nnmordi  6519  genpcdl  7520  genpcuu  7521  mulnqprl  7569  mulnqpru  7570  distrlem1prl  7583  distrlem1pru  7584  divgt0  8831  divge0  8832  uzind2  9367  facdiv  10720  dvdsabseq  11855  divgcdcoprm0  12103  lmodvsdi  13406