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  1228  expdcom  1492  nebidc  2500  sbcimdv  3117  prel12  3894  reusv3  4604  relcoi1  5317  oprabid  6111  poxp  6462  reldmtpos  6518  tfrlem9  6584  tfri3  6632  ordiso2  7369  distrlem5prl  7947  distrlem5pru  7948  bndndx  9545  uzind2  9741  leexp1a  11014  swrdswrdlem  11459  swrdswrd  11460  swrdccat3blem  11494  reuccatpfxs1lem  11501  cncongr1  12864  infpnlem1  13121  gausslemma2dlem1a  16160  uhgr2edg  16430  lealltlt1  16734  bj-inf2vnlem2  16980