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  2563  elpwunsn  4636  onint  7729  tfindsg  7797  findsg  7833  tfrlem9  8310  tz7.49  8370  oaordi  8467  odi  8500  nnaordi  8539  nndi  8544  php  9123  fiint  9218  carduni  9881  dfac2b  10029  axcclem  10355  zorn2lem6  10399  zorn2lem7  10400  grur1a  10717  mulcanpi  10798  ltexprlem7  10940  axpre-sup  11067  xrsupsslem  13208  xrinfmsslem  13209  supxrunb1  13220  supxrunb2  13221  mulgnnass  19024  fiinopn  22817  axcont  28956  sumdmdlem  32400  matunitlindflem1  37676  ee33VD  44995