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 ) ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  84  com35  90  3an1rs  1250  rspct  2922  po2nr  4454  funssres  5420  f1ocnv2d  6294  f1o3d  6298  tfrlem9  6590  nnmass  6760  nnmordi  6789  genpcdl  7886  genpcuu  7887  mulnqprl  7935  mulnqpru  7936  distrlem1prl  7949  distrlem1pru  7950  divgt0  9202  divge0  9203  uzind2  9758  facdiv  11176  swrdswrdlem  11476  wrd2ind  11495  dvdsabseq  12614  divgcdcoprm0  12879  lmodvsdi  14648