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  1355  merco2  1743  onint  7740  oalimcl  8492  oeordsuc  8527  fisup2g  9379  fiinf2g  9412  zorn2lem7  10422  inar1  10696  rpnnen1lem5  12929  expnbnd  14192  facwordi  14249  fi1uzind  14467  brfi1indALT  14470  unbenlem  16877  fiinopn  22891  cmpsublem  23389  dvcnvrelem1  26009  nocvxminlem  27771  onsfi  28373  axcontlem4  29061  axcont  29070  spansncol  31664  atcvat4i  32493  sumdmdlem  32514  broutsideof2  36357  relowlpssretop  37733  cvrat4  39942  pm2.43cbi  44969