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  1243  rspct  2900  po2nr  4400  funssres  5360  f1ocnv2d  6216  tfrlem9  6471  nnmass  6641  nnmordi  6670  genpcdl  7717  genpcuu  7718  mulnqprl  7766  mulnqpru  7767  distrlem1prl  7780  distrlem1pru  7781  divgt0  9030  divge0  9031  uzind2  9570  facdiv  10972  swrdswrdlem  11252  wrd2ind  11271  dvdsabseq  12374  divgcdcoprm0  12639  lmodvsdi  14291