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 ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))

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  102  3expd  1372  mo4  2594  elpwunsn  4651  onint  7790  tfindsg  7858  findsg  7895  tfrlem9  8373  tz7.49  8433  oaordi  8532  odi  8565  nnaordi  8605  nndi  8610  php  9192  fiint  9287  carduni  9968  dfac2b  10115  axcclem  10442  zorn2lem6  10486  zorn2lem7  10487  grur1a  10805  mulcanpi  10886  ltexprlem7  11028  axpre-sup  11155  xrsupsslem  13334  xrinfmsslem  13335  supxrunb1  13346  supxrunb2  13347  mulgnnass  19176  fiinopn  23039  axcont  29304  sumdmdlem  32748  matunitlindflem1  38245  ee33VD  45567