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  1250  rspct  2922  po2nr  4449  funssres  5415  f1ocnv2d  6284  f1o3d  6288  tfrlem9  6580  nnmass  6750  nnmordi  6779  genpcdl  7876  genpcuu  7877  mulnqprl  7925  mulnqpru  7926  distrlem1prl  7939  distrlem1pru  7940  divgt0  9192  divge0  9193  uzind2  9737  facdiv  11154  swrdswrdlem  11454  wrd2ind  11473  dvdsabseq  12592  divgcdcoprm0  12857  lmodvsdi  14620