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  1344  merco2  1733  onint  7509  oalimcl  8185  oeordsuc  8219  fisup2g  8931  fiinf2g  8963  zorn2lem7  9923  inar1  10196  rpnnen1lem5  12379  expnbnd  13592  facwordi  13648  fi1uzind  13854  brfi1indALT  13857  unbenlem  16243  fiinopn  21508  cmpsublem  22006  dvcnvrelem1  24613  axcontlem4  26752  axcont  26761  spansncol  29344  atcvat4i  30173  sumdmdlem  30194  nocvxminlem  33247  broutsideof2  33583  relowlpssretop  34644  cvrat4  36578  pm2.43cbi  40850