Theorem com4l 93

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com4l	⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))

Proof of Theorem com4l

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com3l 90	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏))))
3	2	com34 92	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:  com4t  94  com4r  95  com14  97  com5l  101  3impd  1367  merco2  1769  onint  7792  oalimcl  8550  oeordsuc  8585  fisup2g  9442  fiinf2g  9475  zorn2lem7  10507  inar1  10787  rpnnen1lem5  13033  expnbnd  14298  facwordi  14355  fi1uzind  14574  brfi1indALT  14577  unbenlem  17004  fiinopn  23130  cmpsublem  23628  dvcnvrelem1  26249  nocvxminlem  28020  onsfi  28622  axcontlem4  29425  axcont  29434  spansncol  32050  atcvat4i  32879  sumdmdlem  32900  broutsideof2  36704  relowlpssretop  38120  cvrat4  40318  pm2.43cbi  45343