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  1735  onint  7817  oalimcl  8606  oeordsuc  8640  fisup2g  9515  fiinf2g  9547  zorn2lem7  10549  inar1  10822  rpnnen1lem5  13030  expnbnd  14277  facwordi  14334  fi1uzind  14552  brfi1indALT  14555  unbenlem  16951  fiinopn  22932  cmpsublem  23432  dvcnvrelem1  26082  nocvxminlem  27848  axcontlem4  29008  axcont  29017  spansncol  31613  atcvat4i  32442  sumdmdlem  32463  broutsideof2  36117  relowlpssretop  37359  cvrat4  39440  pm2.43cbi  44531