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  1345  merco2  1730  onint  7792  oalimcl  8579  oeordsuc  8613  fisup2g  9491  fiinf2g  9523  zorn2lem7  10525  inar1  10798  rpnnen1lem5  12995  expnbnd  14226  facwordi  14280  fi1uzind  14490  brfi1indALT  14493  unbenlem  16876  fiinopn  22833  cmpsublem  23333  dvcnvrelem1  25980  nocvxminlem  27740  axcontlem4  28834  axcont  28843  spansncol  31434  atcvat4i  32263  sumdmdlem  32284  broutsideof2  35788  relowlpssretop  36913  cvrat4  38985  pm2.43cbi  44022