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  1350  merco2  1738  onint  7737  oalimcl  8488  oeordsuc  8523  fisup2g  9375  fiinf2g  9408  zorn2lem7  10415  inar1  10689  rpnnen1lem5  12922  expnbnd  14185  facwordi  14242  fi1uzind  14460  brfi1indALT  14463  unbenlem  16870  fiinopn  22876  cmpsublem  23374  dvcnvrelem1  25994  nocvxminlem  27760  onsfi  28362  axcontlem4  29050  axcont  29059  spansncol  31654  atcvat4i  32483  sumdmdlem  32504  broutsideof2  36320  relowlpssretop  37694  cvrat4  39903  pm2.43cbi  44963