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  1348  merco2  1735  onint  7792  oalimcl  8580  oeordsuc  8614  fisup2g  9490  fiinf2g  9522  zorn2lem7  10524  inar1  10797  rpnnen1lem5  13005  expnbnd  14253  facwordi  14310  fi1uzind  14528  brfi1indALT  14531  unbenlem  16928  fiinopn  22855  cmpsublem  23353  dvcnvrelem1  25992  nocvxminlem  27758  axcontlem4  28912  axcont  28921  spansncol  31515  atcvat4i  32344  sumdmdlem  32365  broutsideof2  36082  relowlpssretop  37324  cvrat4  39404  pm2.43cbi  44495