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  1303  merco2  1701  onint  7037  oalimcl  7685  oeordsuc  7719  fisup2g  8415  fiinf2g  8447  zorn2lem7  9362  inar1  9635  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  expnbnd  13033  facwordi  13116  fi1uzind  13317  brfi1indALT  13320  unbenlem  15659  fiinopn  20754  cmpsublem  21250  dvcnvrelem1  23825  axcontlem4  25892  axcont  25901  spansncol  28555  atcvat4i  29384  sumdmdlem  29405  nocvxminlem  32018  broutsideof2  32354  relowlpssretop  33342  cvrat4  35047  pm2.43cbi  39041