Theorem com4l 93

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 90	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏))))
3	2	com34 92	1 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4t  94  com4r  95  com14  97  com5l  101  3impd  1367  merco2  1768  onint  7804  oalimcl  8571  oeordsuc  8606  fisup2g  9464  fiinf2g  9497  zorn2lem7  10583  inar1  10863  rpnnen1lem5  13112  expnbnd  14379  facwordi  14436  fi1uzind  14655  brfi1indALT  14658  unbenlem  17091  fiinopn  23224  cmpsublem  23722  dvcnvrelem1  26342  nocvxminlem  28145  onsfi  28747  axcontlem4  29550  axcont  29559  spansncol  32175  atcvat4i  33004  sumdmdlem  33025  broutsideof2  36979  relowlpssretop  38380  cvrat4  40593  pm2.43cbi  45594