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  1349  merco2  1736  onint  7768  oalimcl  8526  oeordsuc  8560  fisup2g  9426  fiinf2g  9459  zorn2lem7  10461  inar1  10734  rpnnen1lem5  12946  expnbnd  14203  facwordi  14260  fi1uzind  14478  brfi1indALT  14481  unbenlem  16885  fiinopn  22794  cmpsublem  23292  dvcnvrelem1  25928  nocvxminlem  27695  onsfi  28253  axcontlem4  28900  axcont  28909  spansncol  31503  atcvat4i  32332  sumdmdlem  32353  broutsideof2  36105  relowlpssretop  37347  cvrat4  39432  pm2.43cbi  44501