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  1346  merco2  1742  onint  7630  oalimcl  8367  oeordsuc  8401  fisup2g  9188  fiinf2g  9220  zorn2lem7  10242  inar1  10515  rpnnen1lem5  12703  expnbnd  13928  facwordi  13984  fi1uzind  14192  brfi1indALT  14195  unbenlem  16590  fiinopn  22031  cmpsublem  22531  dvcnvrelem1  25162  axcontlem4  27316  axcont  27325  spansncol  29909  atcvat4i  30738  sumdmdlem  30759  nocvxminlem  33951  broutsideof2  34403  relowlpssretop  35514  cvrat4  37436  pm2.43cbi  42091