Theorem com4r 95

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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com4l 93	1 ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com15  102  3expd  1372  mo4  2593  elpwunsn  4648  onint  7793  tfindsg  7861  findsg  7898  tfrlem9  8378  tz7.49  8438  oaordi  8537  odi  8570  nnaordi  8610  nndi  8615  php  9205  fiint  9300  carduni  9990  dfac2b  10137  axcclem  10463  zorn2lem6  10507  zorn2lem7  10508  grur1a  10832  mulcanpi  10913  ltexprlem7  11055  axpre-sup  11182  xrsupsslem  13363  xrinfmsslem  13364  supxrunb1  13375  supxrunb2  13376  mulgnnass  19238  matunitlindflem1  22907  fiinopn  23132  axcont  29441  sumdmdlem  32907  ee33VD  45709