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  1350  mo4  2554  elpwunsn  4689  onint  7794  tfindsg  7866  findsg  7905  tfrlem9  8406  tz7.49  8466  oaordi  8567  odi  8600  nnaordi  8639  nndi  8644  php  9235  phpOLD  9247  fiint  9350  carduni  10006  dfac2b  10155  axcclem  10482  zorn2lem6  10526  zorn2lem7  10527  grur1a  10844  mulcanpi  10925  ltexprlem7  11067  axpre-sup  11194  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  supxrunb2  13334  mulgnnass  19072  fiinopn  22847  axcont  28859  sumdmdlem  32300  matunitlindflem1  37220  ee33VD  44460