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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com4l  84  impd  252  expdcom  1401  nebidc  2362  sbcimdv  2942  prel12  3664  reusv3  4341  relcoi1  5028  oprabid  5757  poxp  6083  reldmtpos  6104  tfrlem9  6170  tfri3  6218  ordiso2  6872  distrlem5prl  7342  distrlem5pru  7343  bndndx  8880  uzind2  9067  leexp1a  10241  cncongr1  11630  bj-inf2vnlem2  12861