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  1736  onint  7766  oalimcl  8524  oeordsuc  8558  fisup2g  9420  fiinf2g  9453  zorn2lem7  10455  inar1  10728  rpnnen1lem5  12940  expnbnd  14197  facwordi  14254  fi1uzind  14472  brfi1indALT  14475  unbenlem  16879  fiinopn  22788  cmpsublem  23286  dvcnvrelem1  25922  nocvxminlem  27689  onsfi  28247  axcontlem4  28894  axcont  28903  spansncol  31497  atcvat4i  32326  sumdmdlem  32347  broutsideof2  36110  relowlpssretop  37352  cvrat4  39437  pm2.43cbi  44508