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  2870  po2nr  4356  funssres  5313  f1ocnv2d  6150  tfrlem9  6405  nnmass  6573  nnmordi  6602  genpcdl  7632  genpcuu  7633  mulnqprl  7681  mulnqpru  7682  distrlem1prl  7695  distrlem1pru  7696  divgt0  8945  divge0  8946  uzind2  9485  facdiv  10883  dvdsabseq  12158  divgcdcoprm0  12423  lmodvsdi  14073