Theorem com4r 95

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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 93	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  102  3expd  1370  mo4  2596  elpwunsn  4646  onint  7777  tfindsg  7845  findsg  7882  tfrlem9  8360  tz7.49  8420  oaordi  8519  odi  8552  nnaordi  8592  nndi  8597  php  9179  fiint  9274  carduni  9955  dfac2b  10102  axcclem  10429  zorn2lem6  10473  zorn2lem7  10474  grur1a  10792  mulcanpi  10873  ltexprlem7  11015  axpre-sup  11142  xrsupsslem  13324  xrinfmsslem  13325  supxrunb1  13336  supxrunb2  13337  mulgnnass  19166  fiinopn  23019  axcont  29235  sumdmdlem  32679  matunitlindflem1  38127  ee33VD  45452