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  1367  merco2  1766  onint  7790  oalimcl  8546  oeordsuc  8581  fisup2g  9430  fiinf2g  9463  zorn2lem7  10487  inar1  10761  rpnnen1lem5  13006  expnbnd  14270  facwordi  14327  fi1uzind  14546  brfi1indALT  14549  unbenlem  16969  fiinopn  23039  cmpsublem  23537  dvcnvrelem1  26157  nocvxminlem  27925  onsfi  28527  axcontlem4  29295  axcont  29304  spansncol  31898  atcvat4i  32727  sumdmdlem  32748  broutsideof2  36592  relowlpssretop  37988  cvrat4  40195  pm2.43cbi  45207