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  1410  merco2  1780  onint  7273  oalimcl  7924  oeordsuc  7958  fisup2g  8662  fiinf2g  8694  zorn2lem7  9659  inar1  9932  rpnnen1lem5  12128  expnbnd  13312  facwordi  13394  fi1uzind  13593  brfi1indALT  13596  unbenlem  16016  fiinopn  21113  cmpsublem  21611  dvcnvrelem1  24217  axcontlem4  26316  axcont  26325  spansncol  28999  atcvat4i  29828  sumdmdlem  29849  nocvxminlem  32482  broutsideof2  32818  relowlpssretop  33807  cvrat4  35597  pm2.43cbi  39678