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  1202  expdcom  1465  nebidc  2460  sbcimdv  3074  prel12  3828  reusv3  4528  relcoi1  5236  oprabid  6006  poxp  6348  reldmtpos  6369  tfrlem9  6435  tfri3  6483  ordiso2  7170  distrlem5prl  7741  distrlem5pru  7742  bndndx  9336  uzind2  9527  leexp1a  10783  swrdswrdlem  11202  swrdswrd  11203  swrdccat3blem  11237  reuccatpfxs1lem  11244  cncongr1  12591  infpnlem1  12848  gausslemma2dlem1a  15702  uhgr2edg  15969  bj-inf2vnlem2  16244