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  1345  merco2  1738  onint  7490  oalimcl  8169  oeordsuc  8203  fisup2g  8916  fiinf2g  8948  zorn2lem7  9913  inar1  10186  rpnnen1lem5  12368  expnbnd  13589  facwordi  13645  fi1uzind  13851  brfi1indALT  13854  unbenlem  16234  fiinopn  21506  cmpsublem  22004  dvcnvrelem1  24620  axcontlem4  26761  axcont  26770  spansncol  29351  atcvat4i  30180  sumdmdlem  30201  nocvxminlem  33360  broutsideof2  33696  relowlpssretop  34781  cvrat4  36739  pm2.43cbi  41224