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  1200  expdcom  1463  nebidc  2457  sbcimdv  3065  prel12  3814  reusv3  4511  relcoi1  5219  oprabid  5983  poxp  6325  reldmtpos  6346  tfrlem9  6412  tfri3  6460  ordiso2  7144  distrlem5prl  7706  distrlem5pru  7707  bndndx  9301  uzind2  9492  leexp1a  10746  swrdswrdlem  11163  swrdswrd  11164  cncongr1  12469  infpnlem1  12726  gausslemma2dlem1a  15579  bj-inf2vnlem2  15981