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 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4l  84  impd  254  3imp231  1221  expdcom  1485  nebidc  2480  sbcimdv  3094  prel12  3849  reusv3  4551  relcoi1  5260  oprabid  6039  poxp  6384  reldmtpos  6405  tfrlem9  6471  tfri3  6519  ordiso2  7210  distrlem5prl  7781  distrlem5pru  7782  bndndx  9376  uzind2  9567  leexp1a  10824  swrdswrdlem  11244  swrdswrd  11245  swrdccat3blem  11279  reuccatpfxs1lem  11286  cncongr1  12633  infpnlem1  12890  gausslemma2dlem1a  15745  uhgr2edg  16012  bj-inf2vnlem2  16358