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  1214  rspct  2827  po2nr  4294  funssres  5240  f1ocnv2d  6053  tfrlem9  6298  nnmass  6466  nnmordi  6495  genpcdl  7481  genpcuu  7482  mulnqprl  7530  mulnqpru  7531  distrlem1prl  7544  distrlem1pru  7545  divgt0  8788  divge0  8789  uzind2  9324  facdiv  10672  dvdsabseq  11807  divgcdcoprm0  12055