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  6865  oalimcl  7505  oeordsuc  7539  fisup2g  8235  fiinf2g  8267  zorn2lem7  9185  inar1  9454  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  expnbnd  12813  facwordi  12896  fi1uzind  13083  brfi1indALT  13086  fi1uzindOLD  13089  brfi1indALTOLD  13092  unbenlem  15399  fiinopn  20479  cmpsublem  20960  dvcnvrelem1  23529  axcontlem4  25593  axcont  25602  spansncol  27605  atcvat4i  28434  sumdmdlem  28455  nocvxminlem  30883  broutsideof2  31193  relowlpssretop  32182  cvrat4  33541  pm2.43cbi  37539