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  1355  mo4  2566  elpwunsn  4628  onint  7744  tfindsg  7812  findsg  7848  tfrlem9  8324  tz7.49  8384  oaordi  8481  odi  8514  nnaordi  8554  nndi  8559  php  9141  fiint  9237  carduni  9905  dfac2b  10053  axcclem  10379  zorn2lem6  10423  zorn2lem7  10424  grur1a  10742  mulcanpi  10823  ltexprlem7  10965  axpre-sup  11092  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  mulgnnass  19085  fiinopn  22866  axcont  29045  sumdmdlem  32489  matunitlindflem1  37937  ee33VD  45305