Theorem com4t 85

Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1

Assertion

Ref	Expression
com4t

Proof of Theorem com4t

Step	Hyp	Ref	Expression
1		com4.1	. . 3
2	1	com4l 84	. 2
3	2	com4l 84	1

Syntax hints:  ->wi 4

This theorem is referenced by:  com4r  86  com24  87  mopickOLD  2357  isofrlem  6236  tfindsg  6695  tfr3  7087  pssnn  7758  dfac5  8530  cfcoflem  8673  isf32lem12  8765  ltexprlem7  9441  dirtr  15866  erclwwlktr  24815  erclwwlkntr  24827  el2wlkonot  24869  3cyclfrgrarn1  25012  frgraregord013  25118  chirredlem1  27309  mdsymlem4  27325  cdj3lem2b  27356  ssfz12  32330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7