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  1355  mo4  2567  elpwunsn  4629  onint  7737  tfindsg  7805  findsg  7841  tfrlem9  8317  tz7.49  8377  oaordi  8474  odi  8507  nnaordi  8547  nndi  8552  php  9134  fiint  9230  carduni  9896  dfac2b  10044  axcclem  10370  zorn2lem6  10414  zorn2lem7  10415  grur1a  10733  mulcanpi  10814  ltexprlem7  10956  axpre-sup  11083  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  mulgnnass  19076  fiinopn  22876  axcont  29059  sumdmdlem  32504  matunitlindflem1  37951  ee33VD  45323