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  2566  elpwunsn  4641  onint  7735  tfindsg  7803  findsg  7839  tfrlem9  8316  tz7.49  8376  oaordi  8473  odi  8506  nnaordi  8546  nndi  8551  php  9131  fiint  9227  carduni  9893  dfac2b  10041  axcclem  10367  zorn2lem6  10411  zorn2lem7  10412  grur1a  10730  mulcanpi  10811  ltexprlem7  10953  axpre-sup  11080  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  mulgnnass  19039  fiinopn  22845  axcont  29049  sumdmdlem  32493  matunitlindflem1  37813  ee33VD  45115