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  2447  sbcimdv  3055  prel12  3802  reusv3  4496  relcoi1  5202  oprabid  5957  poxp  6299  reldmtpos  6320  tfrlem9  6386  tfri3  6434  ordiso2  7110  distrlem5prl  7672  distrlem5pru  7673  bndndx  9267  uzind2  9457  leexp1a  10705  cncongr1  12298  infpnlem1  12555  gausslemma2dlem1a  15385  bj-inf2vnlem2  15703