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  1350  merco2  1738  onint  7744  oalimcl  8495  oeordsuc  8530  fisup2g  9382  fiinf2g  9415  zorn2lem7  10424  inar1  10698  rpnnen1lem5  12931  expnbnd  14194  facwordi  14251  fi1uzind  14469  brfi1indALT  14472  unbenlem  16879  fiinopn  22866  cmpsublem  23364  dvcnvrelem1  25984  nocvxminlem  27746  onsfi  28348  axcontlem4  29036  axcont  29045  spansncol  31639  atcvat4i  32468  sumdmdlem  32489  broutsideof2  36304  relowlpssretop  37680  cvrat4  39889  pm2.43cbi  44945