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  1353  mo4  2559  elpwunsn  4649  onint  7730  tfindsg  7802  findsg  7841  tfrlem9  8336  tz7.49  8396  oaordi  8498  odi  8531  nnaordi  8570  nndi  8575  php  9161  phpOLD  9173  fiint  9275  carduni  9926  dfac2b  10075  axcclem  10402  zorn2lem6  10446  zorn2lem7  10447  grur1a  10764  mulcanpi  10845  ltexprlem7  10987  axpre-sup  11114  xrsupsslem  13236  xrinfmsslem  13237  supxrunb1  13248  supxrunb2  13249  mulgnnass  18925  fiinopn  22287  axcont  27988  sumdmdlem  31423  matunitlindflem1  36147  ee33VD  43283