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  7828  oalimcl  8596  oeordsuc  8631  fisup2g  9488  fiinf2g  9521  zorn2lem7  10607  inar1  10887  rpnnen1lem5  13136  expnbnd  14403  facwordi  14460  fi1uzind  14679  brfi1indALT  14682  unbenlem  17115  fiinopn  23249  cmpsublem  23747  dvcnvrelem1  26367  nocvxminlem  28170  onsfi  28772  axcontlem4  29575  axcont  29584  spansncol  32200  atcvat4i  33029  sumdmdlem  33050  broutsideof2  37065  relowlpssretop  38479  cvrat4  40692  pm2.43cbi  45692