Theorem com4r 95

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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 93	1 ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com15  102  3expd  1372  mo4  2597  elpwunsn  4655  onint  7798  tfindsg  7866  findsg  7903  tfrlem9  8381  tz7.49  8441  oaordi  8540  odi  8573  nnaordi  8613  nndi  8618  php  9201  fiint  9296  carduni  9986  dfac2b  10133  axcclem  10459  zorn2lem6  10503  zorn2lem7  10504  grur1a  10822  mulcanpi  10903  ltexprlem7  11045  axpre-sup  11172  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  supxrunb2  13364  mulgnnass  19206  fiinopn  23095  axcont  29363  sumdmdlem  32807  matunitlindflem1  38308  ee33VD  45628