Theorem com3l 81

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com3l	⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Proof of Theorem com3l

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 79	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 79	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  84  impd  254  3imp231  1228  expdcom  1492  nebidc  2500  sbcimdv  3117  prel12  3896  reusv3  4608  relcoi1  5322  oprabid  6120  poxp  6472  reldmtpos  6528  tfrlem9  6594  tfri3  6642  ordiso2  7382  distrlem5prl  7960  distrlem5pru  7961  bndndx  9574  uzind2  9770  leexp1a  11053  swrdswrdlem  11499  swrdswrd  11500  swrdccat3blem  11534  reuccatpfxs1lem  11541  cncongr1  12907  infpnlem1  13168  gausslemma2dlem1a  16394  uhgr2edg  16664  lealltlt1  16968  bj-inf2vnlem2  17214