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  4643  onint  7745  tfindsg  7813  findsg  7849  tfrlem9  8326  tz7.49  8386  oaordi  8483  odi  8516  nnaordi  8556  nndi  8561  php  9143  fiint  9239  carduni  9905  dfac2b  10053  axcclem  10379  zorn2lem6  10423  zorn2lem7  10424  grur1a  10742  mulcanpi  10823  ltexprlem7  10965  axpre-sup  11092  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  mulgnnass  19051  fiinopn  22857  axcont  29061  sumdmdlem  32505  matunitlindflem1  37861  ee33VD  45228