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  7729  oalimcl  8481  oeordsuc  8515  fisup2g  9360  fiinf2g  9393  zorn2lem7  10400  inar1  10673  rpnnen1lem5  12881  expnbnd  14141  facwordi  14198  fi1uzind  14416  brfi1indALT  14419  unbenlem  16822  fiinopn  22817  cmpsublem  23315  dvcnvrelem1  25950  nocvxminlem  27718  onsfi  28284  axcontlem4  28947  axcont  28956  spansncol  31550  atcvat4i  32379  sumdmdlem  32400  broutsideof2  36187  relowlpssretop  37429  cvrat4  39562  pm2.43cbi  44635