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  7798  oalimcl  8554  oeordsuc  8589  fisup2g  9439  fiinf2g  9472  zorn2lem7  10504  inar1  10778  rpnnen1lem5  13023  expnbnd  14288  facwordi  14345  fi1uzind  14564  brfi1indALT  14567  unbenlem  16993  fiinopn  23095  cmpsublem  23593  dvcnvrelem1  26213  nocvxminlem  27984  onsfi  28586  axcontlem4  29354  axcont  29363  spansncol  31957  atcvat4i  32786  sumdmdlem  32807  broutsideof2  36635  relowlpssretop  38051  cvrat4  40258  pm2.43cbi  45268