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  7745  oalimcl  8497  oeordsuc  8532  fisup2g  9384  fiinf2g  9417  zorn2lem7  10424  inar1  10698  rpnnen1lem5  12906  expnbnd  14167  facwordi  14224  fi1uzind  14442  brfi1indALT  14445  unbenlem  16848  fiinopn  22857  cmpsublem  23355  dvcnvrelem1  25990  nocvxminlem  27762  onsfi  28364  axcontlem4  29052  axcont  29061  spansncol  31655  atcvat4i  32484  sumdmdlem  32505  broutsideof2  36335  relowlpssretop  37613  cvrat4  39813  pm2.43cbi  44868