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  1223  expdcom  1487  nebidc  2481  sbcimdv  3096  prel12  3855  reusv3  4559  relcoi1  5270  oprabid  6055  poxp  6402  reldmtpos  6424  tfrlem9  6490  tfri3  6538  ordiso2  7239  distrlem5prl  7811  distrlem5pru  7812  bndndx  9406  uzind2  9597  leexp1a  10862  swrdswrdlem  11294  swrdswrd  11295  swrdccat3blem  11329  reuccatpfxs1lem  11336  cncongr1  12698  infpnlem1  12955  gausslemma2dlem1a  15816  uhgr2edg  16086  bj-inf2vnlem2  16626