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  1354  mo4  2561  elpwunsn  4688  onint  7778  tfindsg  7850  findsg  7890  tfrlem9  8385  tz7.49  8445  oaordi  8546  odi  8579  nnaordi  8618  nndi  8623  php  9210  phpOLD  9222  fiint  9324  carduni  9976  dfac2b  10125  axcclem  10452  zorn2lem6  10496  zorn2lem7  10497  grur1a  10814  mulcanpi  10895  ltexprlem7  11037  axpre-sup  11164  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  supxrunb2  13299  mulgnnass  18989  fiinopn  22403  axcont  28234  sumdmdlem  31671  matunitlindflem1  36484  ee33VD  43640