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  2560  elpwunsn  4651  onint  7769  tfindsg  7840  findsg  7876  tfrlem9  8356  tz7.49  8416  oaordi  8513  odi  8546  nnaordi  8585  nndi  8590  php  9177  fiint  9284  fiintOLD  9285  carduni  9941  dfac2b  10091  axcclem  10417  zorn2lem6  10461  zorn2lem7  10462  grur1a  10779  mulcanpi  10860  ltexprlem7  11002  axpre-sup  11129  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  mulgnnass  19048  fiinopn  22795  axcont  28910  sumdmdlem  32354  matunitlindflem1  37617  ee33VD  44875