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  2564  elpwunsn  4631  onint  7703  tfindsg  7775  findsg  7814  tfrlem9  8286  tz7.49  8346  oaordi  8448  odi  8481  nnaordi  8520  nndi  8525  php  9075  phpOLD  9087  fiint  9189  carduni  9838  dfac2b  9987  axcclem  10314  zorn2lem6  10358  zorn2lem7  10359  grur1a  10676  mulcanpi  10757  ltexprlem7  10899  axpre-sup  11026  xrsupsslem  13142  xrinfmsslem  13143  supxrunb1  13154  supxrunb2  13155  mulgnnass  18834  fiinopn  22156  axcont  27633  sumdmdlem  31068  matunitlindflem1  35886  ee33VD  42829