Theorem com4r 92

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 91	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 90	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  99  3imp3i2an  1270  3expd  1276  elpwunsn  4171  onint  6887  tfindsg  6952  findsg  6985  tfrlem9  7368  tz7.49  7427  oaordi  7513  odi  7546  nnaordi  7585  nndi  7590  php  8029  fiint  8122  carduni  8690  dfac2  8836  axcclem  9162  zorn2lem6  9206  zorn2lem7  9207  grur1a  9520  mulcanpi  9601  ltexprlem7  9743  axpre-sup  9869  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  mulgnnass  17399  mulgnnassOLD  17400  fiinopn  20531  axcont  25656  sumdmdlem  28661  matunitlindflem1  32575  ee33VD  38137