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  4638  onint  7730  tfindsg  7801  findsg  7837  tfrlem9  8314  tz7.49  8374  oaordi  8471  odi  8504  nnaordi  8543  nndi  8548  php  9131  fiint  9235  fiintOLD  9236  carduni  9896  dfac2b  10044  axcclem  10370  zorn2lem6  10414  zorn2lem7  10415  grur1a  10732  mulcanpi  10813  ltexprlem7  10955  axpre-sup  11082  xrsupsslem  13227  xrinfmsslem  13228  supxrunb1  13239  supxrunb2  13240  mulgnnass  19006  fiinopn  22804  axcont  28939  sumdmdlem  32380  matunitlindflem1  37595  ee33VD  44852