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  1366  mo4  2592  elpwunsn  4642  onint  7769  tfindsg  7837  findsg  7874  tfrlem9  8351  tz7.49  8411  oaordi  8510  odi  8543  nnaordi  8583  nndi  8588  php  9171  fiint  9267  carduni  9936  dfac2b  10084  axcclem  10411  zorn2lem6  10455  zorn2lem7  10456  grur1a  10774  mulcanpi  10855  ltexprlem7  10997  axpre-sup  11124  xrsupsslem  13307  xrinfmsslem  13308  supxrunb1  13319  supxrunb2  13320  mulgnnass  19134  fiinopn  22941  axcont  29123  sumdmdlem  32567  matunitlindflem1  38079  ee33VD  45418