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  1199  expdcom  1453  nebidc  2444  sbcimdv  3051  prel12  3797  reusv3  4491  relcoi1  5197  oprabid  5950  poxp  6285  reldmtpos  6306  tfrlem9  6372  tfri3  6420  ordiso2  7094  distrlem5prl  7646  distrlem5pru  7647  bndndx  9239  uzind2  9429  leexp1a  10665  cncongr1  12241  infpnlem1  12497  gausslemma2dlem1a  15174  bj-inf2vnlem2  15463