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  1349  mo4  2646  elpwunsn  4614  onint  7504  tfindsg  7569  findsg  7603  tfrlem9  8015  tz7.49  8075  oaordi  8166  odi  8199  nnaordi  8238  nndi  8243  php  8695  fiint  8789  carduni  9404  dfac2b  9550  axcclem  9873  zorn2lem6  9917  zorn2lem7  9918  grur1a  10235  mulcanpi  10316  ltexprlem7  10458  axpre-sup  10585  xrsupsslem  12694  xrinfmsslem  12695  supxrunb1  12706  supxrunb2  12707  mulgnnass  18256  fiinopn  21503  axcont  26756  sumdmdlem  30189  matunitlindflem1  34882  ee33VD  41206