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  4648  onint  7766  tfindsg  7837  findsg  7873  tfrlem9  8353  tz7.49  8413  oaordi  8510  odi  8543  nnaordi  8582  nndi  8587  php  9171  fiint  9277  fiintOLD  9278  carduni  9934  dfac2b  10084  axcclem  10410  zorn2lem6  10454  zorn2lem7  10455  grur1a  10772  mulcanpi  10853  ltexprlem7  10995  axpre-sup  11122  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  mulgnnass  19041  fiinopn  22788  axcont  28903  sumdmdlem  32347  matunitlindflem1  37610  ee33VD  44868