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  1360  mo4  2570  elpwunsn  4623  onint  7740  tfindsg  7808  findsg  7844  tfrlem9  8321  tz7.49  8381  oaordi  8478  odi  8511  nnaordi  8551  nndi  8556  php  9138  fiint  9234  carduni  9903  dfac2b  10051  axcclem  10377  zorn2lem6  10421  zorn2lem7  10422  grur1a  10740  mulcanpi  10821  ltexprlem7  10963  axpre-sup  11090  xrsupsslem  13257  xrinfmsslem  13258  supxrunb1  13269  supxrunb2  13270  mulgnnass  19083  fiinopn  22891  axcont  29070  sumdmdlem  32514  matunitlindflem1  37990  ee33VD  45329