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  7793  oalimcl  8552  oeordsuc  8587  fisup2g  9445  fiinf2g  9478  zorn2lem7  10561  inar1  10841  rpnnen1lem5  13090  expnbnd  14356  facwordi  14413  fi1uzind  14632  brfi1indALT  14635  unbenlem  17066  fiinopn  23199  cmpsublem  23697  dvcnvrelem1  26317  nocvxminlem  28122  onsfi  28724  axcontlem4  29527  axcont  29536  spansncol  32152  atcvat4i  32981  sumdmdlem  33002  broutsideof2  36857  relowlpssretop  38255  cvrat4  40468  pm2.43cbi  45460