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  1347  merco2  1739  onint  7640  oalimcl  8391  oeordsuc  8425  fisup2g  9227  fiinf2g  9259  zorn2lem7  10258  inar1  10531  rpnnen1lem5  12721  expnbnd  13947  facwordi  14003  fi1uzind  14211  brfi1indALT  14214  unbenlem  16609  fiinopn  22050  cmpsublem  22550  dvcnvrelem1  25181  axcontlem4  27335  axcont  27344  spansncol  29930  atcvat4i  30759  sumdmdlem  30780  nocvxminlem  33972  broutsideof2  34424  relowlpssretop  35535  cvrat4  37457  pm2.43cbi  42138