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  1346  merco2  1740  onint  7617  oalimcl  8353  oeordsuc  8387  fisup2g  9157  fiinf2g  9189  zorn2lem7  10189  inar1  10462  rpnnen1lem5  12650  expnbnd  13875  facwordi  13931  fi1uzind  14139  brfi1indALT  14142  unbenlem  16537  fiinopn  21958  cmpsublem  22458  dvcnvrelem1  25086  axcontlem4  27238  axcont  27247  spansncol  29831  atcvat4i  30660  sumdmdlem  30681  nocvxminlem  33899  broutsideof2  34351  relowlpssretop  35462  cvrat4  37384  pm2.43cbi  42027