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  1221  rspct  2857  po2nr  4340  funssres  5296  f1ocnv2d  6122  tfrlem9  6372  nnmass  6540  nnmordi  6569  genpcdl  7579  genpcuu  7580  mulnqprl  7628  mulnqpru  7629  distrlem1prl  7642  distrlem1pru  7643  divgt0  8891  divge0  8892  uzind2  9429  facdiv  10809  dvdsabseq  11989  divgcdcoprm0  12239  lmodvsdi  13807