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  1352  mo4  2566  elpwunsn  4619  onint  7640  tfindsg  7707  findsg  7746  tfrlem9  8216  tz7.49  8276  oaordi  8377  odi  8410  nnaordi  8449  nndi  8454  php  8993  phpOLD  9005  fiint  9091  carduni  9739  dfac2b  9886  axcclem  10213  zorn2lem6  10257  zorn2lem7  10258  grur1a  10575  mulcanpi  10656  ltexprlem7  10798  axpre-sup  10925  xrsupsslem  13041  xrinfmsslem  13042  supxrunb1  13053  supxrunb2  13054  mulgnnass  18738  fiinopn  22050  axcont  27344  sumdmdlem  30780  matunitlindflem1  35773  ee33VD  42499