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  1738  onint  7730  oalimcl  8512  oeordsuc  8546  fisup2g  9413  fiinf2g  9445  zorn2lem7  10447  inar1  10720  rpnnen1lem5  12915  expnbnd  14145  facwordi  14199  fi1uzind  14408  brfi1indALT  14411  unbenlem  16791  fiinopn  22287  cmpsublem  22787  dvcnvrelem1  25418  nocvxminlem  27160  axcontlem4  27979  axcont  27988  spansncol  30573  atcvat4i  31402  sumdmdlem  31423  broutsideof2  34783  relowlpssretop  35908  cvrat4  37979  pm2.43cbi  42922