Theorem com4l 90

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 87	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏))))
3	2	com34 89	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  91  com4r  92  com14  94  com5l  98  3impd  1273  merco2  1652  onint  6887  oalimcl  7527  oeordsuc  7561  fisup2g  8257  fiinf2g  8289  zorn2lem7  9207  inar1  9476  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  expnbnd  12855  facwordi  12938  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  unbenlem  15450  fiinopn  20531  cmpsublem  21012  dvcnvrelem1  23584  axcontlem4  25647  axcont  25656  spansncol  27811  atcvat4i  28640  sumdmdlem  28661  nocvxminlem  31089  broutsideof2  31399  relowlpssretop  32388  cvrat4  33747  pm2.43cbi  37745