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  1224  expdcom  1488  nebidc  2494  sbcimdv  3111  prel12  3880  reusv3  4586  relcoi1  5299  oprabid  6090  poxp  6441  reldmtpos  6497  tfrlem9  6563  tfri3  6611  ordiso2  7339  distrlem5prl  7917  distrlem5pru  7918  bndndx  9515  uzind2  9711  leexp1a  10983  swrdswrdlem  11424  swrdswrd  11425  swrdccat3blem  11459  reuccatpfxs1lem  11466  cncongr1  12828  infpnlem1  13085  gausslemma2dlem1a  16060  uhgr2edg  16330  lealltlt1  16634  bj-inf2vnlem2  16880