Theorem com4r 94

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

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com4r	⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

Proof of Theorem com4r

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4t 93	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 92	1 ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

Syntax hints:   → wi 4

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

This theorem is referenced by:  com15  101  3expd  1415  elpwunsn  4452  onint  7275  tfindsg  7340  findsg  7373  tfrlem9  7766  tz7.49  7825  oaordi  7912  odi  7945  nnaordi  7984  nndi  7989  php  8434  fiint  8527  carduni  9142  dfac2b  9288  dfac2OLD  9290  axcclem  9616  zorn2lem6  9660  zorn2lem7  9661  grur1a  9978  mulcanpi  10059  ltexprlem7  10201  axpre-sup  10328  xrsupsslem  12453  xrinfmsslem  12454  supxrunb1  12465  supxrunb2  12466  mulgnnass  17965  fiinopn  21117  axcont  26329  sumdmdlem  29853  matunitlindflem1  34036  ee33VD  40058