Theorem com4r 95

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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 93	1 ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com15  102  3expd  1372  mo4  2591  elpwunsn  4641  onint  7804  tfindsg  7872  findsg  7909  tfrlem9  8396  tz7.49  8458  oaordi  8557  odi  8590  nnaordi  8630  nndi  8635  php  9225  fiint  9321  carduni  10065  dfac2b  10212  axcclem  10538  zorn2lem6  10582  zorn2lem7  10583  grur1a  10907  mulcanpi  10988  ltexprlem7  11130  axpre-sup  11257  xrsupsslem  13440  xrinfmsslem  13441  supxrunb1  13452  supxrunb2  13453  mulgnnass  19324  matunitlindflem1  22999  fiinopn  23224  axcont  29559  sumdmdlem  33025  ee33VD  45954