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  1769  onint  7793  oalimcl  8551  oeordsuc  8586  fisup2g  9443  fiinf2g  9476  zorn2lem7  10508  inar1  10788  rpnnen1lem5  13035  expnbnd  14300  facwordi  14357  fi1uzind  14576  brfi1indALT  14579  unbenlem  17006  fiinopn  23132  cmpsublem  23630  dvcnvrelem1  26251  nocvxminlem  28027  onsfi  28629  axcontlem4  29432  axcont  29441  spansncol  32057  atcvat4i  32886  sumdmdlem  32907  broutsideof2  36710  relowlpssretop  38126  cvrat4  40324  pm2.43cbi  45349