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  2592  elpwunsn  4645  onint  7793  tfindsg  7861  findsg  7898  tfrlem9  8377  tz7.49  8439  oaordi  8538  odi  8571  nnaordi  8611  nndi  8616  php  9206  fiint  9302  carduni  10043  dfac2b  10190  axcclem  10516  zorn2lem6  10560  zorn2lem7  10561  grur1a  10885  mulcanpi  10966  ltexprlem7  11108  axpre-sup  11235  xrsupsslem  13418  xrinfmsslem  13419  supxrunb1  13430  supxrunb2  13431  mulgnnass  19299  matunitlindflem1  22974  fiinopn  23199  axcont  29536  sumdmdlem  33002  ee33VD  45820