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  2914  po2nr  4430  funssres  5395  f1ocnv2d  6259  tfrlem9  6550  nnmass  6720  nnmordi  6749  genpcdl  7834  genpcuu  7835  mulnqprl  7883  mulnqpru  7884  distrlem1prl  7897  distrlem1pru  7898  divgt0  9146  divge0  9147  uzind2  9690  facdiv  11100  swrdswrdlem  11396  wrd2ind  11415  dvdsabseq  12533  divgcdcoprm0  12798  lmodvsdi  14459