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  2594  elpwunsn  4645  onint  7828  tfindsg  7896  findsg  7933  tfrlem9  8421  tz7.49  8483  oaordi  8582  odi  8615  nnaordi  8655  nndi  8660  php  9250  fiint  9346  carduni  10089  dfac2b  10236  axcclem  10562  zorn2lem6  10606  zorn2lem7  10607  grur1a  10931  mulcanpi  11012  ltexprlem7  11154  axpre-sup  11281  xrsupsslem  13464  xrinfmsslem  13465  supxrunb1  13476  supxrunb2  13477  mulgnnass  19348  matunitlindflem1  23024  fiinopn  23249  axcont  29584  sumdmdlem  33050  ee33VD  46052