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  2565  elpwunsn  4660  onint  7784  tfindsg  7856  findsg  7893  tfrlem9  8399  tz7.49  8459  oaordi  8558  odi  8591  nnaordi  8630  nndi  8635  php  9221  phpOLD  9231  fiint  9338  fiintOLD  9339  carduni  9995  dfac2b  10145  axcclem  10471  zorn2lem6  10515  zorn2lem7  10516  grur1a  10833  mulcanpi  10914  ltexprlem7  11056  axpre-sup  11183  xrsupsslem  13323  xrinfmsslem  13324  supxrunb1  13335  supxrunb2  13336  mulgnnass  19092  fiinopn  22839  axcont  28955  sumdmdlem  32399  matunitlindflem1  37640  ee33VD  44903