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  7730  oalimcl  8485  oeordsuc  8519  fisup2g  9378  fiinf2g  9411  zorn2lem7  10415  inar1  10688  rpnnen1lem5  12900  expnbnd  14157  facwordi  14214  fi1uzind  14432  brfi1indALT  14435  unbenlem  16838  fiinopn  22804  cmpsublem  23302  dvcnvrelem1  25938  nocvxminlem  27706  onsfi  28270  axcontlem4  28930  axcont  28939  spansncol  31530  atcvat4i  32359  sumdmdlem  32380  broutsideof2  36095  relowlpssretop  37337  cvrat4  39422  pm2.43cbi  44492