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  1737  onint  7735  oalimcl  8487  oeordsuc  8522  fisup2g  9372  fiinf2g  9405  zorn2lem7  10412  inar1  10686  rpnnen1lem5  12894  expnbnd  14155  facwordi  14212  fi1uzind  14430  brfi1indALT  14433  unbenlem  16836  fiinopn  22845  cmpsublem  23343  dvcnvrelem1  25978  nocvxminlem  27750  onsfi  28352  axcontlem4  29040  axcont  29049  spansncol  31643  atcvat4i  32472  sumdmdlem  32493  broutsideof2  36316  relowlpssretop  37565  cvrat4  39699  pm2.43cbi  44755