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  1222  rspct  2877  po2nr  4374  funssres  5332  f1ocnv2d  6173  tfrlem9  6428  nnmass  6596  nnmordi  6625  genpcdl  7667  genpcuu  7668  mulnqprl  7716  mulnqpru  7717  distrlem1prl  7730  distrlem1pru  7731  divgt0  8980  divge0  8981  uzind2  9520  facdiv  10920  swrdswrdlem  11195  wrd2ind  11214  dvdsabseq  12273  divgcdcoprm0  12538  lmodvsdi  14188