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  4552  relcoi1  5263  oprabid  6042  poxp  6389  reldmtpos  6410  tfrlem9  6476  tfri3  6524  ordiso2  7218  distrlem5prl  7789  distrlem5pru  7790  bndndx  9384  uzind2  9575  leexp1a  10833  swrdswrdlem  11257  swrdswrd  11258  swrdccat3blem  11292  reuccatpfxs1lem  11299  cncongr1  12646  infpnlem1  12903  gausslemma2dlem1a  15758  uhgr2edg  16025  bj-inf2vnlem2  16443