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  1197  expdcom  1442  nebidc  2427  sbcimdv  3029  prel12  3772  reusv3  4461  relcoi1  5161  oprabid  5907  poxp  6233  reldmtpos  6254  tfrlem9  6320  tfri3  6368  ordiso2  7034  distrlem5prl  7585  distrlem5pru  7586  bndndx  9175  uzind2  9365  leexp1a  10575  cncongr1  12103  infpnlem1  12357  bj-inf2vnlem2  14726