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  1353  mo4  2569  elpwunsn  4707  onint  7826  tfindsg  7898  findsg  7937  tfrlem9  8441  tz7.49  8501  oaordi  8602  odi  8635  nnaordi  8674  nndi  8679  php  9273  phpOLD  9285  fiint  9394  fiintOLD  9395  carduni  10050  dfac2b  10200  axcclem  10526  zorn2lem6  10570  zorn2lem7  10571  grur1a  10888  mulcanpi  10969  ltexprlem7  11111  axpre-sup  11238  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  supxrunb2  13382  mulgnnass  19149  fiinopn  22928  axcont  29009  sumdmdlem  32450  matunitlindflem1  37576  ee33VD  44850