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  1246  rspct  2904  po2nr  4412  funssres  5376  f1ocnv2d  6237  tfrlem9  6528  nnmass  6698  nnmordi  6727  genpcdl  7799  genpcuu  7800  mulnqprl  7848  mulnqpru  7849  distrlem1prl  7862  distrlem1pru  7863  divgt0  9111  divge0  9112  uzind2  9653  facdiv  11063  swrdswrdlem  11351  wrd2ind  11370  dvdsabseq  12488  divgcdcoprm0  12753  lmodvsdi  14407