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  1351  mo4  2566  elpwunsn  4616  onint  7617  tfindsg  7682  findsg  7720  tfrlem9  8187  tz7.49  8246  oaordi  8339  odi  8372  nnaordi  8411  nndi  8416  php  8897  fiint  9021  carduni  9670  dfac2b  9817  axcclem  10144  zorn2lem6  10188  zorn2lem7  10189  grur1a  10506  mulcanpi  10587  ltexprlem7  10729  axpre-sup  10856  xrsupsslem  12970  xrinfmsslem  12971  supxrunb1  12982  supxrunb2  12983  mulgnnass  18653  fiinopn  21958  axcont  27247  sumdmdlem  30681  matunitlindflem1  35700  ee33VD  42388