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  3110  prel12  3877  reusv3  4583  relcoi1  5296  oprabid  6084  poxp  6430  reldmtpos  6486  tfrlem9  6552  tfri3  6600  ordiso2  7328  distrlem5prl  7906  distrlem5pru  7907  bndndx  9500  uzind2  9696  leexp1a  10963  swrdswrdlem  11404  swrdswrd  11405  swrdccat3blem  11439  reuccatpfxs1lem  11446  cncongr1  12808  infpnlem1  13065  gausslemma2dlem1a  15980  uhgr2edg  16250  bj-inf2vnlem2  16790