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  1361  merco2  1755  onint  7769  oalimcl  8524  oeordsuc  8559  fisup2g  9412  fiinf2g  9445  zorn2lem7  10456  inar1  10730  rpnnen1lem5  12979  expnbnd  14242  facwordi  14299  fi1uzind  14517  brfi1indALT  14520  unbenlem  16927  fiinopn  22941  cmpsublem  23439  dvcnvrelem1  26059  nocvxminlem  27824  onsfi  28426  axcontlem4  29114  axcont  29123  spansncol  31717  atcvat4i  32546  sumdmdlem  32567  broutsideof2  36436  relowlpssretop  37822  cvrat4  40031  pm2.43cbi  45058