Theorem com4l 92

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 89	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏))))
3	2	com34 91	1 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4t  93  com4r  94  com14  96  com5l  100  3impd  1349  merco2  1737  onint  7723  oalimcl  8475  oeordsuc  8509  fisup2g  9353  fiinf2g  9386  zorn2lem7  10390  inar1  10663  rpnnen1lem5  12876  expnbnd  14136  facwordi  14193  fi1uzind  14411  brfi1indALT  14414  unbenlem  16817  fiinopn  22814  cmpsublem  23312  dvcnvrelem1  25947  nocvxminlem  27715  onsfi  28281  axcontlem4  28943  axcont  28952  spansncol  31543  atcvat4i  32372  sumdmdlem  32393  broutsideof2  36155  relowlpssretop  37397  cvrat4  39481  pm2.43cbi  44550