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  1351  mo4  2558  elpwunsn  4688  onint  7782  tfindsg  7854  findsg  7894  tfrlem9  8389  tz7.49  8449  oaordi  8550  odi  8583  nnaordi  8622  nndi  8627  php  9214  phpOLD  9226  fiint  9328  carduni  9980  dfac2b  10129  axcclem  10456  zorn2lem6  10500  zorn2lem7  10501  grur1a  10818  mulcanpi  10899  ltexprlem7  11041  axpre-sup  11168  xrsupsslem  13292  xrinfmsslem  13293  supxrunb1  13304  supxrunb2  13305  mulgnnass  19027  fiinopn  22625  axcont  28499  sumdmdlem  31936  matunitlindflem1  36789  ee33VD  43944