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  2561  elpwunsn  4637  onint  7723  tfindsg  7791  findsg  7827  tfrlem9  8304  tz7.49  8364  oaordi  8461  odi  8494  nnaordi  8533  nndi  8538  php  9116  fiint  9211  carduni  9871  dfac2b  10019  axcclem  10345  zorn2lem6  10389  zorn2lem7  10390  grur1a  10707  mulcanpi  10788  ltexprlem7  10930  axpre-sup  11057  xrsupsslem  13203  xrinfmsslem  13204  supxrunb1  13215  supxrunb2  13216  mulgnnass  19019  fiinopn  22814  axcont  28952  sumdmdlem  32393  matunitlindflem1  37655  ee33VD  44910