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  9204  divge0  9205  uzind2  9762  facdiv  11190  swrdswrdlem  11490  wrd2ind  11509  dvdsabseq  12630  divgcdcoprm0  12895  lmodvsdi  14697