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  1355  mo4  2565  elpwunsn  4585  onint  7552  tfindsg  7617  findsg  7655  tfrlem9  8099  tz7.49  8159  oaordi  8252  odi  8285  nnaordi  8324  nndi  8329  php  8808  fiint  8926  carduni  9562  dfac2b  9709  axcclem  10036  zorn2lem6  10080  zorn2lem7  10081  grur1a  10398  mulcanpi  10479  ltexprlem7  10621  axpre-sup  10748  xrsupsslem  12862  xrinfmsslem  12863  supxrunb1  12874  supxrunb2  12875  mulgnnass  18480  fiinopn  21752  axcont  27021  sumdmdlem  30453  matunitlindflem1  35459  ee33VD  42113