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  1354  mo4  2559  elpwunsn  4636  onint  7726  tfindsg  7794  findsg  7830  tfrlem9  8307  tz7.49  8367  oaordi  8464  odi  8497  nnaordi  8536  nndi  8541  php  9121  fiint  9216  fiintOLD  9217  carduni  9877  dfac2b  10025  axcclem  10351  zorn2lem6  10395  zorn2lem7  10396  grur1a  10713  mulcanpi  10794  ltexprlem7  10936  axpre-sup  11063  xrsupsslem  13209  xrinfmsslem  13210  supxrunb1  13221  supxrunb2  13222  mulgnnass  18988  fiinopn  22786  axcont  28925  sumdmdlem  32366  matunitlindflem1  37616  ee33VD  44872