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  1361  mo4  2572  elpwunsn  4618  onint  7736  tfindsg  7804  findsg  7841  tfrlem9  8318  tz7.49  8378  oaordi  8475  odi  8508  nnaordi  8548  nndi  8553  php  9135  fiint  9231  carduni  9900  dfac2b  10048  axcclem  10375  zorn2lem6  10419  zorn2lem7  10420  grur1a  10738  mulcanpi  10819  ltexprlem7  10961  axpre-sup  11088  xrsupsslem  13254  xrinfmsslem  13255  supxrunb1  13266  supxrunb2  13267  mulgnnass  19080  fiinopn  22887  axcont  29065  sumdmdlem  32509  matunitlindflem1  37996  ee33VD  45335