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  1245  rspct  2903  po2nr  4406  funssres  5369  f1ocnv2d  6226  tfrlem9  6484  nnmass  6654  nnmordi  6683  genpcdl  7738  genpcuu  7739  mulnqprl  7787  mulnqpru  7788  distrlem1prl  7801  distrlem1pru  7802  divgt0  9051  divge0  9052  uzind2  9591  facdiv  10999  swrdswrdlem  11284  wrd2ind  11303  dvdsabseq  12407  divgcdcoprm0  12672  lmodvsdi  14324