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 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))

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  94  com4r  95  com14  97  com5l  101  3impd  1365  merco2  1759  onint  7777  oalimcl  8533  oeordsuc  8568  fisup2g  9417  fiinf2g  9450  zorn2lem7  10474  inar1  10748  rpnnen1lem5  12996  expnbnd  14259  facwordi  14316  fi1uzind  14534  brfi1indALT  14537  unbenlem  16958  fiinopn  23019  cmpsublem  23517  dvcnvrelem1  26137  nocvxminlem  27905  onsfi  28507  axcontlem4  29226  axcont  29235  spansncol  31829  atcvat4i  32658  sumdmdlem  32679  broutsideof2  36485  relowlpssretop  37870  cvrat4  40079  pm2.43cbi  45092